1  /-
  2  Copyright (c) 2018 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Jens Wagemaker
  5  
  6  Theory of unique factorization domains.
  7  
  8  @TODO: setup the complete lattice structure on `factor_set`.
  9  -/
 10  import algebra.gcd_domain
src         └────────────────┘
 11  
 12  variables {α : Type*}
id             
typ            
 13  local infix ` ~ᵤ ` : 50 := associated
id                              └────────┘
src                             └────────┘
typ                             └────────┘
 14  
 15  /-- Unique factorization domains.
 16  
 17  In a unique factorization domain each element (except zero) is uniquely
 18  represented as a multiset of irreducible factors.
 19  Uniqueness is only up to associated elements.
 20  
 21  This is equivalent to defining a unique factorization domain as a domain in
 22  which each element (except zero) is non-uniquely represented as a multiset
 23  of prime factors. This definition is used.
 24  
 25  To define a UFD using the traditional definition in terms of multisets
 26  of irreducible factors, use the definition `of_unique_irreducible_factorization`
 27  
 28  -/
 29  class unique_factorization_domain (α : Type*) [integral_domain α] :=
id                                          └───┘   └─────────────┘ 
src                                                 └─────────────┘
typ                                         └───┘   └─────────────┘ 
 30  (factors : α → multiset α)
id                └──────┘ 
src                 └──────┘
typ               └──────┘ 
doc                 └──────┘
 31  (factors_prod : ∀{a : α}, a ≠ 0 → (factors a).prod ~ᵤ a)
id                                  └─────┘  └──┘  └┘ 
src                                              └──┘  └┘
typ                                 └─────┘  └──┘  └┘ 
doc                                               └──┘
 32  (prime_factors : ∀{a : α}, a ≠ 0 → ∀x∈factors a, prime x)
id                                    └─────┘   └───┘ 
src                                                 └───┘
typ                                   └─────┘   └───┘ 
doc                                                   └───┘
 33  
 34  namespace unique_factorization_domain
 35  
 36  variables [integral_domain α] [unique_factorization_domain α]
id              └─────────────┘     └─────────────────────────┘
src             └─────────────┘     └─────────────────────────┘
typ             └─────────────┘     └─────────────────────────┘
doc                                 └─────────────────────────┘
 37  
 38  @[elab_as_eliminator] lemma induction_on_prime {P : α → Prop}
id                                                       
typ                                                      
doc    └────────────────┘
 39    (a : α) (h₁ : P 0) (h₂ : ∀ x : α, is_unit x → P x)
id                                    └─────┘     
src                                      └─────┘
typ                                   └─────┘     
doc                                      └─────┘
 40    (h₃ : ∀ a p : α, a ≠ 0 → prime p → P a → P (p * a)) : P a :=
id                           └───┘                  
src                            └───┘                
typ                          └───┘                  
doc                             └───┘
 41  by haveI := classical.dec_eq α; exact
id               └──────────────┘ 
src     └───────┘└──────────────┘   └────┘
typ     └───────┘└──────────────┘  └────┘
doc     └───────┘                   └────┘
txt     └───────┘                   └────┘
par     └───────┘                   └────┘
pid          └─┘                        
st     └───────────────────────────────────
 42  if ha0 : a = 0 then ha0.symm ▸ h₁
id   └┘                    └───┘  └┘
src  └┘└─────┘ └──────┘   └───┘  
typ  └┘└─────┘ └──────┘   └───┘└┘
doc    └─────┘  └──────┘           
txt    └─────┘  └──────┘           
par    └─────┘  └──────┘           
pid    └─────┘  └──────┘           
st   ──────────────────────────────────
 43  else @multiset.induction_on _
id         └───────────────────┘
src  ────┘ └───────────────────┘└──
typ  ────┘ └───────────────────┘└──
doc  ────┘                      └──
txt  ────┘                      └──
par  ────┘                      └──
pid  ────┘                      └──
st   ──────────────────────────────
 44    (λ s : multiset α, ∀ (a : α), a ≠ 0 → s.prod ~ᵤ a → (∀ p ∈ s, prime p) →  P a)
id            └──────┘                      └───┘ └┘               └───┘       
src  ─┘  └───┘└──────┘ └┘ └────┘   └─┘  └───┘└┘    └───┘  └───┘ └┘ └┘  └─
typ  ─┘  └───┘└──────┘ └┘ └────┘  └─┘  └───┘└┘    └───┘  └───┘ └┘ └┘ └─
doc  ─┘  └───┘└──────┘ └┘ └────┘    └─┘  └───┘      └───┘  └───┘ └┘ └┘  └─
txt  ─┘  └───┘         └┘ └────┘    └─┘             └───┘        └┘ └┘  └─
par  ─┘  └───┘         └┘ └────┘    └─┘             └───┘        └┘ └┘  └─
pid  ─┘  └───┘         └┘ └────┘    └─┘             └───┘        └┘ └┘  └─
st   ─────────────────────────────────────────────────────────────────────────────────
 45    (factors a)
id      └─────┘ 
src  ─┘ └─────┘ └─
typ  ─┘ └─────┘└─
doc  ─┘         └─
txt  ─┘         └─
par  ─┘         └─
pid  ─┘         └─
st   ──────────────
 46    (λ _ _ h _, h₂ _ ((is_unit_iff_of_associated h.symm).2 is_unit_one))
id                 └┘     └───────────────────────┘  └───┘    └─────────┘
src  ─┘  └────────┘  └─┘  └───────────────────────┘ └───┘└──┘└─────────┘└──
typ  ─┘  └────────┘└┘└─┘  └───────────────────────┘ └───┘└──┘└─────────┘└──
doc  ─┘  └────────┘  └─┘                                 └──┘           └──
txt  ─┘  └────────┘  └─┘                                 └──┘           └──
par  ─┘  └────────┘  └─┘                                 └──┘           └──
pid  ─┘  └────────┘  └─┘                                 └──┘           └──
st   ───────────────────────────────────────────────────────────────────────
 47    (λ p s ih a ha0 ⟨u, hu⟩ hsp,
id                      
src  ─┘  └─────────────┘ └┘  └──────
typ  ─┘  └─────────────┘└┘  └──────
doc  ─┘  └─────────────┘ └┘  └──────
txt  ─┘  └─────────────┘ └┘  └──────
par  ─┘  └─────────────┘ └┘  └──────
pid  ─┘  └─────────────┘ └┘  └──────
st   ───────────────────────────────
 48      have ha : a = (p * u) * s.prod, by simp [hu.symm, mul_comm, mul_assoc],
id                               └───┘                    └──────┘  └───────┘
src  ───┘    └────┘      └┘ └───┘└───┘└────┘       └┘└──────┘└┘└───────┘└─
typ  ───┘    └────┘      └┘ └───┘└───┘└────┘└─────┘└┘└──────┘└┘└───────┘└─
doc  ───┘    └────┘      └┘  └───┘└───┘└────┘       └┘        └┘         └─
txt  ───┘    └────┘      └┘       └───┘└────┘       └┘        └┘         └─
par  ───┘    └────┘      └┘       └───┘└────┘       └┘        └┘         └─
pid  ───┘    └────┘      └┘       └─────────┘       └┘        └┘         └──
st   ─────────────────────────────────────┘└──────────────────────────────────┘└─
 49      have hs0 : s.prod ≠ 0, from λ _ : s.prod = 0, by simp * at *,
id                   └───┘                        
src  ───┘    └─────┘ └───┘ └───────┘ └───┘       └──┘  └─────────┘└─
typ  ───┘    └─────┘ └───┘ └───────┘ └───┘      └──┘  └─────────┘└─
doc  ───┘    └─────┘ └───┘ └───────┘ └───┘       └──┘  └─────────┘└─
txt  ───┘    └─────┘       └───────┘ └───┘       └──┘  └─────────┘└─
par  ───┘    └─────┘       └───────┘ └───┘       └──┘  └─────────┘└─
pid  ───┘    └─────┘       └───────┘ └───┘       └──┘  └─────────────
st   ───────────────────────────────────────────────────┘└──────────┘└─
 50      ha.symm ▸ h₃ _ _ hs0
id                 └┘
src  ───┘          └───┘   
typ  ───┘        └┘└───┘   
doc  ───┘          └───┘   
txt  ───┘          └───┘   
par  ───┘          └───┘   
pid  ───┘          └───┘   
st   ─────────────────────────
 51        (prime_of_associated ⟨u, rfl⟩ (hsp p (multiset.mem_cons_self _ _)))
id          └─────────────────┘     └─┘         └────────────────────┘
src  ─────┘ └─────────────────┘  └┘└─┘└┘      └────────────────────┘└───────
typ  ─────┘ └─────────────────┘  └┘└─┘└┘     └────────────────────┘└───────
doc  ─────┘                      └┘   └┘                            └───────
txt  ─────┘                      └┘   └┘                            └───────
par  ─────┘                      └┘   └┘                            └───────
pid  ─────┘                      └┘   └┘                            └───────
st   ──────────────────────────────────────────────────────────────────────────
 52        (ih _ hs0 (by refl) (λ p hp, hsp p (multiset.mem_cons.2 (or.inr hp)))))
id                                             └───────────────┘    └────┘
src  ─────┘   └─┘      └──┘└┘  └─────┘     └───────────────┘└─┘ └────┘  └─────
typ  ─────┘   └─┘      └──┘└┘  └─────┘     └───────────────┘└─┘ └────┘  └─────
doc  ─────┘   └─┘      └──┘└┘  └─────┘                      └─┘         └─────
txt  ─────┘   └─┘      └──┘└┘  └─────┘                      └─┘         └─────
par  ─────┘   └─┘      └──┘└┘  └─────┘                      └─┘         └─────
pid  ─────┘   └─┘      └─────┘  └─────┘                      └─┘         └─────
st   ──────────────────┘└───┘└─────────────────────────────────────────────────────
 53    _
src  ────
typ  ────
doc  ────
txt  ────
par  ────
pid  ────
st   ────
 54    ha0
src  ─┘   
typ  ─┘   
doc  ─┘   
txt  ─┘   
par  ─┘   
pid  ─┘   
st   ──────
 55    (factors_prod ha0)
id      └──────────┘
src  ─┘ └──────────┘   └─
typ  ─┘ └──────────┘   └─
doc  ─┘                └─
txt  ─┘                └─
par  ─┘                └─
pid  ─┘                └─
st   ─────────────────────
 56    (prime_factors ha0)
id      └───────────┘
src  ─┘ └───────────┘   └─
typ  ─┘ └───────────┘   └─
doc  ─┘                 └─
txt  ─┘                 └─
par  ─┘                 └─
pid  ─┘                 
st   ──────────────────────
 57  
src  
typ  
doc  
txt  
par  
pid  
st   
 58  lemma factors_irreducible {a : α} (ha : irreducible a) :
id                                          └─────────┘ 
src                                          └─────────┘
typ                                         └─────────┘ 
doc                                          └─────────┘
 59    ∃ p, a ~ᵤ p ∧ factors a = p :: 0 :=
id        └┘   └─────┘    └┘
src         └┘    └─────┘      └┘
typ       └┘   └─────┘    └┘
doc                                └┘
 60  by haveI := classical.dec_eq α; exact
id               └──────────────┘ 
src     └───────┘└──────────────┘   └────┘
typ     └───────┘└──────────────┘  └────┘
doc     └───────┘                   └────┘
txt     └───────┘                   └────┘
par     └───────┘                   └────┘
pid          └─┘                        
st     └───────────────────────────────────
 61  multiset.induction_on (factors a)
id   └───────────────────┘  └─────┘ 
src  └───────────────────┘ └─────┘ └─
typ  └───────────────────┘ └─────┘└─
doc                                └─
txt                                └─
par                                └─
pid                                └─
st   ──────────────────────────────────
 62    (λ h, (ha.1 (associated_one_iff_is_unit.1 h.symm)).elim)
id                  └────────────────────────┘    └───┘
src  ─┘  └──┘   └─┘ └────────────────────────┘└─┘ └───┘└────────
typ  ─┘  └──┘   └─┘ └────────────────────────┘└─┘ └───┘└────────
doc  ─┘  └──┘   └─┘                           └─┘      └────────
txt  ─┘  └──┘   └─┘                           └─┘      └────────
par  ─┘  └──┘   └─┘                           └─┘      └────────
pid  ─┘  └──┘   └─┘                           └─┘      └────────
st   ───────────────────────────────────────────────────────────
 63    (λ p s _ hp hs, let ⟨u, hu⟩ := hp in ⟨p,
id                          
src  ─┘  └────────────┘     └┘  └───┘  └──┘  └─
typ  ─┘  └────────────┘    └┘  └───┘  └──┘  └─
doc  ─┘  └────────────┘     └┘  └───┘  └──┘  └─
txt  ─┘  └────────────┘     └┘  └───┘  └──┘  └─
par  ─┘  └────────────┘     └┘  └───┘  └──┘  └─
pid  ─┘  └────────────┘     └┘  └───┘  └──┘  └─
st   ───────────────────────────────────────────
 64      have hs0 : s = 0, from classical.by_contradiction
id                             └────────────────────────┘
src  ───┘    └─────┘ └───────┘└────────────────────────┘
typ  ───┘    └─────┘ └───────┘└────────────────────────┘
doc  ───┘    └─────┘  └───────┘                          
txt  ───┘    └─────┘  └───────┘                          
par  ───┘    └─────┘  └───────┘                          
pid  ───┘    └─────┘  └───────┘                          
st   ──────────────────────────────────────────────────────
 65        (λ hs0, let ⟨q, hq⟩ := multiset.exists_mem_of_ne_zero hs0 in
id                               └────────────────────────────┘
src  ─────┘  └────┘     └┘  └───┘└────────────────────────────┘   └───
typ  ─────┘  └────┘    └┘  └───┘└────────────────────────────┘   └───
doc  ─────┘  └────┘     └┘  └───┘                                 └───
txt  ─────┘  └────┘     └┘  └───┘                                 └───
par  ─────┘  └────┘     └┘  └───┘                                 └───
pid  ─────┘  └────┘     └┘  └───┘                                 └───
st   ───────────────────────────────────────────────────────────────────
 66         (hs q (by simp [hq])).2.1 $
id                          └┘
src  ──────┘       └────┘  └─────┘ 
typ  ──────┘       └────┘└┘└─────┘ 
doc  ──────┘       └────┘  └─────┘ 
txt  ──────┘       └────┘  └─────┘ 
par  ──────┘       └────┘  └─────┘ 
pid  ──────┘       └─────┘  └──────┘ 
st   ───────────────┘└────────┘└────────
 67          (ha.2 ((p * u) * (s.erase q).prod) _
id                           └────┘
src  ───────┘   └─┘     └┘  └────┘ └─────────
typ  ───────┘   └─┘    └┘ └────┘ └─────────
doc  ───────┘   └─┘     └┘   └────┘ └─────────
txt  ───────┘   └─┘     └┘          └─────────
par  ───────┘   └─┘     └┘          └─────────
pid  ───────┘   └─┘     └┘          └─────────
st   ─────────────────────────────────────────────
 68            (by rw [mul_right_comm _ _ q, mul_assoc, ← multiset.prod_cons,
id                     └────────────┘       └───────┘    └────────────────┘
src  ─────────┘   └──┘└────────────┘└───┘ └┘└───────┘└──┘└────────────────┘└─
typ  ─────────┘   └──┘└────────────┘└───┘└┘└───────┘└──┘└────────────────┘└─
doc  ─────────┘   └──┘              └───┘ └┘         └──┘                  └─
txt  ─────────┘   └──┘              └───┘ └┘         └──┘                  └─
par  ─────────┘   └──┘              └───┘ └┘         └──┘                  └─
pid  ─────────┘   └───┘              └───┘ └┘         └──┘                  └─
st   ────────────┘└───────────────────────┘└─────────┘└────────────────────┘└─
 69              multiset.cons_erase hq]; simp [hu.symm, mul_comm, mul_assoc])).resolve_left $
id               └─────────────────┘ └┘                  └──────┘  └───────┘
src  ───────────┘└─────────────────┘  └┘└────┘       └┘└──────┘└┘└───────┘└──────────────┘ 
typ  ───────────┘└─────────────────┘└┘└┘└────┘└─────┘└┘└──────┘└┘└───────┘└──────────────┘ 
doc  ───────────┘                     └┘└────┘       └┘        └┘         └──────────────┘ 
txt  ───────────┘                     └┘└────┘       └┘        └┘         └──────────────┘ 
par  ───────────┘                     └┘└────┘       └┘        └┘         └──────────────┘ 
pid  ───────────┘                     └───────┘       └┘        └┘         └───────────────┘ 
st   ─────────────────────────────────┘└───────────────────────────────────┘└─────────────────
 70                mt is_unit_of_mul_is_unit_left $ mt is_unit_of_mul_is_unit_left
id                                                  └┘ └─────────────────────────┘
src  ─────────────┘                              └┘└─────────────────────────┘
typ  ─────────────┘                              └┘└─────────────────────────┘
doc  ─────────────┘                                                           
txt  ─────────────┘                                                           
par  ─────────────┘                                                           
pid  ─────────────┘                                                           
st   ──────────────────────────────────────────────────────────────────────────────
 71                  (hs p (multiset.mem_cons_self _ _)).2.1),
id                          └────────────────────┘
src  ───────────────┘     └────────────────────┘└────────────
typ  ───────────────┘     └────────────────────┘└────────────
doc  ───────────────┘                           └────────────
txt  ───────────────┘                           └────────────
par  ───────────────┘                           └────────────
pid  ───────────────┘                           └────────────
st   ──────────────────────────────────────────────────────────
 72      ⟨associated.symm (by clear _let_match; simp * at *), hs0 ▸ rfl⟩⟩)
id        └─────────────┘                                          └─┘
src  ───┘ └─────────────┘   └──────────────┘└┘└─────────┘└─┘   └─┘└───
typ  ───┘ └─────────────┘   └──────────────┘└┘└─────────┘└─┘   └─┘└───
doc  ───┘                   └──────────────┘└┘└─────────┘└─┘       └───
txt  ───┘                   └──────────────┘└┘└─────────┘└─┘       └───
par  ───┘                   └──────────────┘└┘└─────────┘└─┘       └───
pid  ───┘                   └───────────────────────────────┘       └───
st   ───────────────────────┘└────────────────────────────┘└───────────────
 73    (factors_prod ha.ne_zero)
id      └──────────┘
src  ─┘ └──────────┘          └─
typ  ─┘ └──────────┘          └─
doc  ─┘                       └─
txt  ─┘                       └─
par  ─┘                       └─
pid  ─┘                       └─
st   ────────────────────────────
 74    (prime_factors ha.ne_zero)
id      └───────────┘ └────────┘
src  ─┘ └───────────┘└────────┘└─
typ  ─┘ └───────────┘└────────┘└─
doc  ─┘                        └─
txt  ─┘                        └─
par  ─┘                        └─
pid  ─┘                        
st   ─────────────────────────────
 75  
src  
typ  
doc  
txt  
par  
pid  
st   
 76  lemma irreducible_iff_prime {p : α} : irreducible p ↔ prime p :=
id                                        └─────────┘   └───┘ 
src                                        └─────────┘    └───┘
typ                                       └─────────┘   └───┘ 
doc                                        └─────────┘     └───┘
 77  by letI := classical.dec_eq α; exact
id              └──────────────┘ 
src     └──────┘└──────────────┘   └────┘
typ     └──────┘└──────────────┘  └────┘
doc     └──────┘                   └────┘
txt     └──────┘                   └────┘
par     └──────┘                   └────┘
pid         └─┘                        
st     └──────────────────────────────────
 78  if hp0 : p = 0 then by simp [hp0]
id   └┘                          └─┘
src  └┘└─────┘ └──────┘  └────┘   └┘
typ  └┘└─────┘ └──────┘  └────┘└─┘└┘
doc    └─────┘  └──────┘  └────┘   └┘
txt    └─────┘  └──────┘  └────┘   └┘
par    └─────┘  └──────┘  └────┘   └┘
pid    └─────┘  └──────┘  └─────┘   └─
st   ─────────────────────┘└──────────┘
 79  else
src  └────
typ  └────
doc  └────
txt  └────
par  └────
pid  ─────
st   └────
 80    ⟨λ h, let ⟨q, hq⟩ := factors_irreducible h in
id                 └┘     └─────────────────┘
src  ─┘  └──┘     └┘  └───┘└─────────────────┘ └───
typ  ─┘ └──┘    └┘└┘└───┘└─────────────────┘ └───
doc  ─┘  └──┘     └┘  └───┘                    └───
txt  ─┘  └──┘     └┘  └───┘                    └───
par  ─┘  └──┘     └┘  └───┘                    └───
pid  ─┘  └──┘     └┘  └───┘                    └───
st   ────────────────────────────────────────────────
 81        have prime q, from hq.2 ▸ prime_factors hp0 _ (by simp [hq.2]),
id                                   └───────────┘                 └┘
src  ─────┘    └─────┘ └─────┘  └─┘ └───────────┘   └─┘   └────┘  └─┘└──
typ  ─────┘    └─────┘ └─────┘  └─┘ └───────────┘   └─┘   └────┘└┘└─┘└──
doc  ─────┘    └─────┘ └─────┘  └─┘                 └─┘   └────┘  └─┘└──
txt  ─────┘    └─────┘ └─────┘  └─┘                 └─┘   └────┘  └─┘└──
par  ─────┘    └─────┘ └─────┘  └─┘                 └─┘   └────┘  └─┘└──
pid  ─────┘    └─────┘ └─────┘  └─┘                 └─┘   └─────┘  └─────
st   ──────────────────────────────────────────────────────┘└──────────┘└──
 82        suffices prime (factors p).prod,
id                         └─────┘ 
src  ─────┘        └─────┘ └─────┘ └───────
typ  ─────┘        └─────┘ └─────┘└───────
doc  ─────┘        └─────┘         └───────
txt  ─────┘        └─────┘         └───────
par  ─────┘        └─────┘         └───────
pid  ─────┘        └─────┘         └───────
st   ───────────────────────────────────────
 83          from prime_of_associated (factors_prod hp0) this,
id                └─────────────────┘  └──────────┘
src  ────────────┘└─────────────────┘ └──────────┘   └┘    └─
typ  ────────────┘└─────────────────┘ └──────────┘   └┘    └─
doc  ────────────┘                                   └┘    └─
txt  ────────────┘                                   └┘    └─
par  ────────────┘                                   └┘    └─
pid  ────────────┘                                   └┘    └─
st   ──────────────────────────────────────────────────────────
 84        hq.2.symm ▸ by simp [this],
id                             └──┘
src  ─────┘  └──────┘  └────┘    └─
typ  ─────┘  └──────┘  └────┘└──┘└─
doc  ─────┘  └──────┘   └────┘    └─
txt  ─────┘  └──────┘   └────┘    └─
par  ─────┘  └──────┘   └────┘    └─
pid  ─────┘  └──────┘   └─────┘    └──
st   ───────────────────┘└──────────┘└─
 85      irreducible_of_prime⟩
id       └──────────────────┘
src  ───┘└──────────────────┘└─
typ  ───┘└──────────────────┘└─
doc  ───┘                    └─
txt  ───┘                    └─
par  ───┘                    └─
pid  ───┘                    
st   ──────────────────────────
 86  
src  
typ  
doc  
txt  
par  
pid  
st   
 87  lemma irreducible_factors : ∀{a : α}, a ≠ 0 → ∀x∈factors a, irreducible x :=
id                                                └─────┘   └─────────┘ 
src                                                  └─────┘    └─────────┘
typ                                               └─────┘   └─────────┘ 
doc                                                              └─────────┘
 88  by simp only [irreducible_iff_prime]; exact @prime_factors _ _ _
id                 └───────────────────┘          └───────────┘
src     └─────────┘└───────────────────┘  └────┘ └───────────┘└──────
typ     └─────────┘└───────────────────┘  └────┘ └───────────┘└──────
doc     └─────────┘                       └────┘              └──────
txt     └─────────┘                       └────┘              └──────
par     └─────────┘                       └────┘              └──────
pid         └──┘└┘                                          └────┘
st     └──────────────────────────────────────────────────────────────
 89  
src  
typ  
doc  
txt  
par  
pid  
st   
 90  lemma unique : ∀{f g : multiset α},
id                          └──────┘ 
src                         └──────┘
typ                         └──────┘ 
doc                         └──────┘
 91    (∀x∈f, irreducible x) → (∀x∈g, irreducible x) → f.prod ~ᵤ g.prod →
id          └─────────┘          └─────────┘     └───┘ └┘ └───┘
src           └─────────┘             └─────────┘       └───┘ └┘  └───┘
typ         └─────────┘          └─────────┘     └───┘ └┘ └───┘
doc           └─────────┘             └─────────┘       └───┘     └───┘
 92    multiset.rel associated f g :=
id     └──────────┘ └────────┘  
src    └──────────┘ └────────┘
typ    └──────────┘ └────────┘  
doc    └──────────┘
 93  by haveI := classical.dec_eq α; exact
id               └──────────────┘ 
src     └───────┘└──────────────┘   └────┘
typ     └───────┘└──────────────┘  └────┘
doc     └───────┘                   └────┘
txt     └───────┘                   └────┘
par     └───────┘                   └────┘
pid          └─┘                        
st     └───────────────────────────────────
 94  λ f, multiset.induction_on f
id        └───────────────────┘
src   └──┘└───────────────────┘ 
typ   └──┘└───────────────────┘ 
doc   └──┘                      
txt   └──┘                      
par   └──┘                      
pid   └──┘                      
st   ─────────────────────────────
 95    (λ g _ hg h,
src  ─┘  └──────────
typ  ─┘  └──────────
doc  ─┘  └──────────
txt  ─┘  └──────────
par  ─┘  └──────────
pid  ─┘  └──────────
st   ───────────────
 96      multiset.rel_zero_left.2 $
id       └────────────────────┘
src  ───┘└────────────────────┘└─┘ 
typ  ───┘└────────────────────┘└─┘ 
doc  ───┘                      └─┘ 
txt  ───┘                      └─┘ 
par  ───┘                      └─┘ 
pid  ───┘                      └─┘ 
st   ───────────────────────────────
 97        multiset.eq_zero_of_forall_not_mem (λ x hx,
id         └────────────────────────────────┘
src  ─────┘└────────────────────────────────┘  └──────
typ  ─────┘└────────────────────────────────┘  └──────
doc  ─────┘                                    └──────
txt  ─────┘                                    └──────
par  ─────┘                                    └──────
pid  ─────┘                                    └──────
st   ──────────────────────────────────────────────────
 98          have is_unit g.prod, by simpa [associated_one_iff_is_unit] using h.symm,
id                         └───┘            └────────────────────────┘        └────┘
src  ───────┘    └───────┘ └───┘└───┘└─────┘└────────────────────────┘└──────┘└────┘└─
typ  ───────┘    └───────┘ └───┘└───┘└─────┘└────────────────────────┘└──────┘└────┘└─
doc  ───────┘    └───────┘ └───┘└───┘└─────┘                          └──────┘      └─
txt  ───────┘    └───────┘      └───┘└─────┘                          └──────┘      └─
par  ───────┘    └───────┘      └───┘└─────┘                          └──────┘      └─
pid  ───────┘    └───────┘      └──────────┘                          └──────┘      └─
st   ──────────────────────────────┘└──────────────────────────────────────────────┘└─
 99          (hg x hx).1 (is_unit_iff_dvd_one.2 (dvd.trans (multiset.dvd_prod hx)
id                                               └───────┘  └───────────────┘
src  ───────┘      └──┘                    └─┘ └───────┘ └───────────────┘  └─
typ  ───────┘      └──┘                    └─┘ └───────┘ └───────────────┘  └─
doc  ───────┘      └──┘                    └─┘                              └─
txt  ───────┘      └──┘                    └─┘                              └─
par  ───────┘      └──┘                    └─┘                              └─
pid  ───────┘      └──┘                    └─┘                              └─
st   ─────────────────────────────────────────────────────────────────────────────
100            (is_unit_iff_dvd_one.1 this)))))
id              └─────────────────┘
src  ─────────┘ └─────────────────┘└─┘    └─────
typ  ─────────┘ └─────────────────┘└─┘    └─────
doc  ─────────┘                    └─┘    └─────
txt  ─────────┘                    └─┘    └─────
par  ─────────┘                    └─┘    └─────
pid  ─────────┘                    └─┘    └─────
st   ───────────────────────────────────────────
101    (λ p f ih g hf hg hfg,
src  ─┘  └────────────────────
typ  ─┘  └────────────────────
doc  ─┘  └────────────────────
txt  ─┘  └────────────────────
par  ─┘  └────────────────────
pid  ─┘  └────────────────────
st   ─────────────────────────
102      let ⟨b, hbg, hb⟩ := exists_associated_mem_of_dvd_prod
id                           └───────────────────────────────┘
src  ───┘     └┘   └┘  └───┘└───────────────────────────────┘
typ  ───┘     └┘   └┘  └───┘└───────────────────────────────┘
doc  ───┘     └┘   └┘  └───┘                                 
txt  ───┘     └┘   └┘  └───┘                                 
par  ───┘     └┘   └┘  └───┘                                 
pid  ───┘     └┘   └┘  └───┘                                 
st   ──────────────────────────────────────────────────────────
103        (irreducible_iff_prime.1 (hf p (by simp)))
src  ─────┘                      └─┘       └──┘└───
typ  ─────┘                      └─┘       └──┘└───
doc  ─────┘                      └─┘       └──┘└───
txt  ─────┘                      └─┘       └──┘└───
par  ─────┘                      └─┘       └──┘└───
pid  ─────┘                      └─┘       └────────
st   ───────────────────────────────────────┘└───┘└───
104        (λ q hq, irreducible_iff_prime.1 (hg _ hq)) $
id                  └───────────────────┘
src  ─────┘  └─────┘└───────────────────┘└─┘   └─┘  └─┘ 
typ  ─────┘  └─────┘└───────────────────┘└─┘   └─┘  └─┘ 
doc  ─────┘  └─────┘                     └─┘   └─┘  └─┘ 
txt  ─────┘  └─────┘                     └─┘   └─┘  └─┘ 
par  ─────┘  └─────┘                     └─┘   └─┘  └─┘ 
pid  ─────┘  └─────┘                     └─┘   └─┘  └─┘ 
st   ────────────────────────────────────────────────────
105          (dvd_iff_dvd_of_rel_right hfg).1
id            └──────────────────────┘
src  ───────┘ └──────────────────────┘   └───
typ  ───────┘ └──────────────────────┘   └───
doc  ───────┘                            └───
txt  ───────┘                            └───
par  ───────┘                            └───
pid  ───────┘                            └───
st   ─────────────────────────────────────────
106            (show p ∣ (p :: f).prod, by simp) in
id                         └┘
src  ─────────┘        └┘ └─────────┘└──┘└────
typ  ─────────┘        └┘ └─────────┘└──┘└────
doc  ─────────┘         └┘ └─────────┘└──┘└────
txt  ─────────┘            └─────────┘└──┘└────
par  ─────────┘            └─────────┘└──┘└────
pid  ─────────┘            └───────────────────
st   ────────────────────────────────────┘└───┘└────
107      begin
src  ───┘     
typ  ───┘     
doc  ───┘     
txt  ───┘     
par  ───┘     
pid  ───┘     
st   ───┘└─────
108        rw ← multiset.cons_erase hbg,
id              └─────────────────┘ └─┘
src  ─────┘└───┘└─────────────────┘   └─
typ  ─────┘└───┘└─────────────────┘└─┘└─
doc  ─────┘└───┘                      └─
txt  ─────┘└───┘                      └─
par  ─────┘└───┘                      └─
pid  ──────────┘                      └─
st   ─────────────────────────────────┘└─
109        exact multiset.rel.cons hb (ih (λ q hq, hf _ (by simp [hq]))
id               └───────────────┘     └┘                         └┘
src  ───────────┘└───────────────┘       └─────┘  └─┘   └────┘  └──
typ  ───────────┘└───────────────┘   └┘  └─────┘  └─┘   └────┘└┘└──
doc  ───────────┘                        └─────┘  └─┘   └────┘  └──
txt  ───────────┘                        └─────┘  └─┘   └────┘  └──
par  ───────────┘                        └─────┘  └─┘   └────┘  └──
pid  ───────────┘                        └─────┘  └─┘   └─────┘  └───
st   ─────────────────────────────────────────────────────┘└────────┘└──
110          (λ q (hq : q ∈ g.erase b), hg q (multiset.mem_of_mem_erase hq))
id                         └─────┘    └┘    └───────────────────────┘
src  ───────┘  └───────┘ └─────┘ └─┘    └───────────────────────┘  └──
typ  ───────┘  └───────┘ └─────┘└─┘└┘  └───────────────────────┘  └──
doc  ───────┘  └───────┘  └─────┘ └─┘                               └──
txt  ───────┘  └───────┘          └─┘                               └──
par  ───────┘  └───────┘          └─┘                               └──
pid  ───────┘  └───────┘          └─┘                               └──
st   ────────────────────────────────────────────────────────────────────────
111          (associated_mul_left_cancel
id            └────────────────────────┘
src  ───────┘ └────────────────────────┘
typ  ───────┘ └────────────────────────┘
doc  ───────┘                           
txt  ───────┘                           
par  ───────┘                           
pid  ───────┘                           
st   ────────────────────────────────────
112            (by rwa [← multiset.prod_cons, ← multiset.prod_cons, multiset.cons_erase hbg]) hb
id                        └────────────────┘    └────────────────┘  └─────────────────┘ └─┘   └┘
src  ─────────┘   └─────┘└────────────────┘└──┘└────────────────┘└┘└─────────────────┘   └┘  
typ  ─────────┘   └─────┘└────────────────┘└──┘└────────────────┘└┘└─────────────────┘└─┘└┘└┘
doc  ─────────┘   └─────┘                  └──┘                  └┘                      └┘  
txt  ─────────┘   └─────┘                  └──┘                  └┘                      └┘  
par  ─────────┘   └─────┘                  └──┘                  └┘                      └┘  
pid  ─────────┘   └──────┘                  └──┘                  └┘                      └─┘  
st   ────────────┘└────────────────────────┘└────────────────────┘└───────────────────────┘└────
113          (hf p (by simp)).ne_zero))
id            └┘ 
src  ───────┘       └──┘└────────────
typ  ───────┘ └┘   └──┘└────────────
doc  ───────┘       └──┘└────────────
txt  ───────┘       └──┘└────────────
par  ───────┘       └──┘└────────────
pid  ───────┘       └─────────────────
st   ────────────────┘└───┘└────────────
114      end)
src  ─────────
typ  ─────────
doc  ─────────
txt  ─────────
par  ─────────
pid  ───────┘
st   ───┘└─┘└─
115  
src  
typ  
doc  
txt  
par  
pid  
st   
116  end unique_factorization_domain
117  
118  structure unique_irreducible_factorization (α : Type*) [integral_domain α] :=
id                                                   └───┘   └─────────────┘ 
src                                                          └─────────────┘
typ                                                  └───┘   └─────────────┘ 
119  (factors : α → multiset α)
id                └──────┘ 
src                 └──────┘
typ               └──────┘ 
doc                 └──────┘
120  (factors_prod : ∀{a : α}, a ≠ 0 → (factors a).prod ~ᵤ a)
id                                  └─────┘  └──┘  └┘ 
src                                              └──┘  └┘
typ                                 └─────┘  └──┘  └┘ 
doc                                               └──┘
121  (irreducible_factors : ∀{a : α}, a ≠ 0 →  ∀x∈factors a, irreducible x)
id                                           └─────┘   └─────────┘ 
src                                                         └─────────┘
typ                                          └─────┘   └─────────┘ 
doc                                                          └─────────┘
122  (unique : ∀{f g : multiset α},
id                    └──────┘ 
src                   └──────┘
typ                   └──────┘ 
doc                    └──────┘
123    (∀x∈f, irreducible x) → (∀x∈g, irreducible x) → f.prod ~ᵤ g.prod → multiset.rel associated f g)
id          └─────────┘          └─────────┘     └───┘ └┘ └───┘   └──────────┘ └────────┘  
src           └─────────┘             └─────────┘       └───┘ └┘  └───┘   └──────────┘ └────────┘
typ         └─────────┘          └─────────┘     └───┘ └┘ └───┘   └──────────┘ └────────┘  
doc           └─────────┘             └─────────┘       └───┘     └───┘   └──────────┘
124  
125  namespace unique_factorization_domain
126  open unique_factorization_domain associated lattice
127  variables [integral_domain α] [unique_factorization_domain α] [decidable_eq (associates α)]
id              └─────────────┘     └─────────────────────────┘     └──────────┘  └────────┘
src             └─────────────┘     └─────────────────────────┘     └──────────┘  └────────┘
typ             └─────────────┘     └─────────────────────────┘     └──────────┘  └────────┘
doc                                 └─────────────────────────┘
128  
129  lemma exists_mem_factors_of_dvd {a p : α} (ha0 : a ≠ 0) (hp : irreducible p) : p ∣ a →
id                                                              └─────────┘       
src                                                               └─────────┘        
typ                                                             └─────────┘       
doc                                                                └─────────┘
130    ∃ q ∈ factors a, p ~ᵤ q :=
id         └─────┘   └┘ 
src         └─────┘     └┘
typ        └─────┘   └┘ 
131  λ ⟨b, hb⟩,
id       └┘
typ      └┘
132  have hb0 : b ≠ 0, from λ hb0, by simp * at *,
id                           └─┘
src                                  └─────────┘
typ                          └─┘     └─────────┘
doc                                   └─────────┘
txt                                   └─────────┘
par                                   └─────────┘
pid                                       └──┘
st                                   └──────────┘
133  have multiset.rel associated (p :: factors b) (factors a),
id        └──────────┘ └────────┘   └┘ └─────┘     └─────┘ 
src       └──────────┘ └────────┘    └┘ └─────┘     └─────┘
typ       └──────────┘ └────────┘   └┘ └─────┘     └─────┘ 
doc       └──────────┘               └┘
134    from unique
id          └────┘
src         └────┘
typ         └────┘
135      (λ x hx, (multiset.mem_cons.1 hx).elim (λ h, h.symm ▸ hp)
id           └┘   └───────────────┘  └┘ └──┘       └───┘  └┘
src                └───────────────┘     └──┘         └───┘ 
typ          └┘   └───────────────┘  └┘ └──┘       └───┘  └┘
136        (irreducible_factors hb0 _))
id          └─────────────────┘ └─┘
src         └─────────────────┘
typ         └─────────────────┘ └─┘
137      (irreducible_factors ha0)
id        └─────────────────┘ └─┘
src       └─────────────────┘
typ       └─────────────────┘ └─┘
138      (associated.symm $ calc multiset.prod (factors a) ~ᵤ a : factors_prod ha0
id        └─────────────┘        └───────────┘  └─────┘         └──────────┘ └─┘
src       └─────────────┘        └───────────┘  └─────┘           └──────────┘
typ       └─────────────┘        └───────────┘  └─────┘         └──────────┘ └─┘
doc                              └───────────┘
139        ... = p * b : hb
id                
src                
typ               
140        ... ~ᵤ multiset.prod (p :: factors b) :
id                └───────────┘   └┘ └─────┘
src               └───────────┘    └┘ └─────┘
typ               └───────────┘   └┘ └─────┘
doc               └───────────┘    └┘
141          by rw multiset.prod_cons; exact associated_mul_mul
id                 └────────────────┘        └────────────────┘
src             └─┘└────────────────┘  └────┘└────────────────┘
typ             └─┘└────────────────┘  └────┘└────────────────┘
doc             └─┘                    └────┘                  
txt             └─┘                    └────┘                  
par             └─┘                    └────┘                  
pid                                                          
st             └────────────────────────────────────────────────
142            (associated.refl _)
id              └─────────────┘
src  ─────────┘ └─────────────┘└───
typ  ─────────┘ └─────────────┘└───
doc  ─────────┘                └───
txt  ─────────┘                └───
par  ─────────┘                └───
pid  ─────────┘                └───
st   ──────────────────────────────
143            (associated.symm (factors_prod hb0))),
id              └─────────────┘  └──────────┘ └─┘
src  ─────────┘ └─────────────┘ └──────────┘   └┘
typ  ─────────┘ └─────────────┘ └──────────┘└─┘└┘
doc  ─────────┘                                └┘
txt  ─────────┘                                └┘
par  ─────────┘                                └┘
pid  ─────────┘                                └┘
st   ─────────────────────────────────────────────┘
144  multiset.exists_mem_of_rel_of_mem this (by simp)
id   └───────────────────────────────┘ └──┘
src  └───────────────────────────────┘          └──┘
typ  └───────────────────────────────┘ └──┘     └──┘
doc                                             └──┘
txt                                             └──┘
par                                             └──┘
st                                             └───┘
145  
146  def of_unique_irreducible_factorization {α : Type*} [integral_domain α]
id                                                        └─────────────┘ 
src                                                       └─────────────┘
typ                                                       └─────────────┘ 
147    (o : unique_irreducible_factorization α) : unique_factorization_domain α :=
id          └──────────────────────────────┘     └─────────────────────────┘ 
src         └──────────────────────────────┘      └─────────────────────────┘
typ         └──────────────────────────────┘     └─────────────────────────┘ 
doc                                               └─────────────────────────┘
148  by letI := classical.dec_eq α; exact
id              └──────────────┘ 
src     └──────┘└──────────────┘   └────┘
typ     └──────┘└──────────────┘  └────┘
doc     └──────┘                   └────┘
txt     └──────┘                   └────┘
par     └──────┘                   └────┘
pid         └─┘                        
st     └──────────────────────────────────
149  { prime_factors := λ a h p (hpa : p ∈ o.factors a),
id                                       
src   └────────────────┘ └────────────┘           └──
typ   └────────────────┘ └────────────┘           └──
doc   └────────────────┘ └────────────┘            └──
txt   └────────────────┘ └────────────┘            └──
par   └────────────────┘ └────────────┘            └──
pid   └────────────────┘ └────────────┘            └──
st   ────────────────────────────────────────────────────
150      have hpi : irreducible p, from o.irreducible_factors h _ hpa,
id                                      └───────────────────┘
src  ───┘    └─────┘            └─────┘└───────────────────┘ └─┘   └─
typ  ───┘    └─────┘            └─────┘└───────────────────┘ └─┘   └─
doc  ───┘    └─────┘            └─────┘                      └─┘   └─
txt  ───┘    └─────┘            └─────┘                      └─┘   └─
par  ───┘    └─────┘            └─────┘                      └─┘   └─
pid  ───┘    └─────┘            └─────┘                      └─┘   └─
st   ──────────────────────────────────────────────────────────────────
151      ⟨hpi.ne_zero, hpi.1,
id           └──────┘
src  ───┘    └──────┘└┘   └───
typ  ───┘    └──────┘└┘   └───
doc  ───┘            └┘   └───
txt  ───┘            └┘   └───
par  ───┘            └┘   └───
pid  ───┘            └┘   └───
st   ─────────────────────────
152        λ a b ⟨x, hx⟩,
id                
src  ─────┘ └────┘ └┘  └──
typ  ─────┘ └────┘└┘  └──
doc  ─────┘ └────┘ └┘  └──
txt  ─────┘ └────┘ └┘  └──
par  ─────┘ └────┘ └┘  └──
pid  ─────┘ └────┘ └┘  └──
st   ─────────────────────
153        if hab0 : a * b = 0
id         └┘             
src  ─────┘└┘└──────┘  └──
typ  ─────┘└┘└──────┘  └──
doc  ─────┘  └──────┘    └──
txt  ─────┘  └──────┘    └──
par  ─────┘  └──────┘    └──
pid  ─────┘  └──────┘    └──
st   ──────────────────────────
154        then (eq_zero_or_eq_zero_of_mul_eq_zero hab0).elim
id               └───────────────────────────────┘
src  ──────────┘ └───────────────────────────────┘    └──────
typ  ──────────┘ └───────────────────────────────┘    └──────
doc  ──────────┘                                      └──────
txt  ──────────┘                                      └──────
par  ──────────┘                                      └──────
pid  ──────────┘                                      └──────
st   ─────────────────────────────────────────────────────────
155          (λ ha0, by simp [ha0])
id                            └─┘
src  ───────┘  └────┘  └────┘   └─
typ  ───────┘  └────┘  └────┘└─┘└─
doc  ───────┘  └────┘  └────┘   └─
txt  ───────┘  └────┘  └────┘   └─
par  ───────┘  └────┘  └────┘   └─
pid  ───────┘  └────┘  └─────┘   └──
st   ─────────────────┘└─────────┘└─
156          (λ hb0, by simp [hb0])
id                            └─┘
src  ───────┘  └────┘  └────┘   └─
typ  ───────┘  └────┘  └────┘└─┘└─
doc  ───────┘  └────┘  └────┘   └─
txt  ───────┘  └────┘  └────┘   └─
par  ───────┘  └────┘  └────┘   └─
pid  ───────┘  └────┘  └─────┘   └──
st   ─────────────────┘└─────────┘└─
157        else
src  ───────────
typ  ───────────
doc  ───────────
txt  ───────────
par  ───────────
pid  ───────────
st   ───────────
158          have hx0 : x ≠ 0, from λ hx0, by simp * at *,
id           └──┘         
src  ───────┘    └─────┘ └───────┘ └────┘  └─────────┘└─
typ  ───────┘└──┘└─────┘ └───────┘ └────┘  └─────────┘└─
doc  ───────┘    └─────┘  └───────┘ └────┘  └─────────┘└─
txt  ───────┘    └─────┘  └───────┘ └────┘  └─────────┘└─
par  ───────┘    └─────┘  └───────┘ └────┘  └─────────┘└─
pid  ───────┘    └─────┘  └───────┘ └────┘  └─────────────
st   ───────────────────────────────────────┘└──────────┘└─
159          have ha0 : a ≠ 0, from ne_zero_of_mul_ne_zero_right hab0,
id                                  └──────────────────────────┘
src  ───────┘    └─────┘  └───────┘└──────────────────────────┘    └─
typ  ───────┘    └─────┘  └───────┘└──────────────────────────┘    └─
doc  ───────┘    └─────┘  └───────┘                                └─
txt  ───────┘    └─────┘  └───────┘                                └─
par  ───────┘    └─────┘  └───────┘                                └─
pid  ───────┘    └─────┘  └───────┘                                └─
st   ──────────────────────────────────────────────────────────────────
160          have hb0 : b ≠ 0, from ne_zero_of_mul_ne_zero_left hab0,
id                                  └─────────────────────────┘
src  ───────┘    └─────┘  └───────┘└─────────────────────────┘    └─
typ  ───────┘    └─────┘  └───────┘└─────────────────────────┘    └─
doc  ───────┘    └─────┘  └───────┘                               └─
txt  ───────┘    └─────┘  └───────┘                               └─
par  ───────┘    └─────┘  └───────┘                               └─
pid  ───────┘    └─────┘  └───────┘                               └─
st   ─────────────────────────────────────────────────────────────────
161          have multiset.rel associated  (p :: o.factors x) (o.factors a + o.factors b),
id                             └────────┘     └┘                           
src  ───────┘    └────────────┘└────────┘└┘  └┘          └┘                     └──
typ  ───────┘    └────────────┘└────────┘└┘  └┘          └┘                     └──
doc  ───────┘    └────────────┘          └┘  └┘          └┘                      └──
txt  ───────┘    └────────────┘          └┘              └┘                      └──
par  ───────┘    └────────────┘          └┘              └┘                      └──
pid  ───────┘    └────────────┘          └┘              └┘                      └──
st   ──────────────────────────────────────────────────────────────────────────────────────
162            from o.unique
id                  └──────┘
src  ──────────────┘└──────┘
typ  ──────────────┘└──────┘
doc  ──────────────┘        
txt  ──────────────┘        
par  ──────────────┘        
pid  ──────────────┘        
st   ────────────────────────
163              (λ i hi, (multiset.mem_cons.1 hi).elim
id                         └───────────────┘
src  ───────────┘  └─────┘ └───────────────┘└─┘  └──────
typ  ───────────┘  └─────┘ └───────────────┘└─┘  └──────
doc  ───────────┘  └─────┘                  └─┘  └──────
txt  ───────────┘  └─────┘                  └─┘  └──────
par  ───────────┘  └─────┘                  └─┘  └──────
pid  ───────────┘  └─────┘                  └─┘  └──────
st   ───────────────────────────────────────────────────
164                (λ hip, hip.symm ▸ hpi)
id                            └───┘ 
src  ─────────────┘  └────┘   └───┘   └─
typ  ─────────────┘  └────┘   └───┘   └─
doc  ─────────────┘  └────┘            └─
txt  ─────────────┘  └────┘            └─
par  ─────────────┘  └────┘            └─
pid  ─────────────┘  └────┘            └─
st   ──────────────────────────────────────
165                (o.irreducible_factors hx0 _))
src  ─────────────┘                         └────
typ  ─────────────┘                         └────
doc  ─────────────┘                         └────
txt  ─────────────┘                         └────
par  ─────────────┘                         └────
pid  ─────────────┘                         └────
st   ─────────────────────────────────────────────
166              (show ∀ x ∈ o.factors a + o.factors b, irreducible x,
id                                                      └─────────┘
src  ───────────┘      └───┘                      └─────────┘ └─
typ  ───────────┘      └───┘                      └─────────┘ └─
doc  ───────────┘      └───┘                      └─────────┘ └─
txt  ───────────┘      └───┘                                  └─
par  ───────────┘      └───┘                                  └─
pid  ───────────┘      └───┘                                  └─
st   ──────────────────────────────────────────────────────────────────
167                from λ x hx, (multiset.mem_add.1 hx).elim
id                               └──────────────┘
src  ──────────────────┘ └─────┘ └──────────────┘└─┘  └──────
typ  ──────────────────┘ └─────┘ └──────────────┘└─┘  └──────
doc  ──────────────────┘ └─────┘                 └─┘  └──────
txt  ──────────────────┘ └─────┘                 └─┘  └──────
par  ──────────────────┘ └─────┘                 └─┘  └──────
pid  ──────────────────┘ └─────┘                 └─┘  └──────
st   ────────────────────────────────────────────────────────
168                  (o.irreducible_factors (ne_zero_of_mul_ne_zero_right hab0) _)
src  ───────────────┘                                                       └────
typ  ───────────────┘                                                       └────
doc  ───────────────┘                                                       └────
txt  ───────────────┘                                                       └────
par  ───────────────┘                                                       └────
pid  ───────────────┘                                                       └────
st   ──────────────────────────────────────────────────────────────────────────────
169                  (o.irreducible_factors (ne_zero_of_mul_ne_zero_left hab0) _)) $
src  ───────────────┘                                                      └────┘ 
typ  ───────────────┘                                                      └────┘ 
doc  ───────────────┘                                                      └────┘ 
txt  ───────────────┘                                                      └────┘ 
par  ───────────────┘                                                      └────┘ 
pid  ───────────────┘                                                      └────┘ 
st   ────────────────────────────────────────────────────────────────────────────────
170                calc multiset.prod (p :: o.factors x)
id                      └───────────┘
src  ─────────────┘    └───────────┘              └─
typ  ─────────────┘    └───────────┘              └─
doc  ─────────────┘    └───────────┘              └─
txt  ─────────────┘                               └─
par  ─────────────┘                               └─
pid  ─────────────┘                               └─
st   ────────────────────────────────────────────────────
171                    ~ᵤ a * b : by rw [hx, multiset.prod_cons];
id                                       └┘  └────────────────┘
src  ─────────────────┘     └─┘  └──┘  └┘└────────────────┘└─
typ  ─────────────────┘     └─┘  └──┘└┘└┘└────────────────┘└─
doc  ─────────────────┘     └─┘  └──┘  └┘                  └─
txt  ─────────────────┘     └─┘  └──┘  └┘                  └─
par  ─────────────────┘     └─┘  └──┘  └┘                  └─
pid  ─────────────────┘     └─┘  └───┘  └┘                  └──
st   ──────────────────────────────┘└─────┘└──────────────────┘└─
172                      exact associated_mul_mul (by refl)
id                             └────────────────┘
src  ─────────────────────────┘└────────────────┘   └──┘└─
typ  ─────────────────────────┘└────────────────┘   └──┘└─
doc  ─────────────────────────┘                     └──┘└─
txt  ─────────────────────────┘                     └──┘└─
par  ─────────────────────────┘                     └──┘└─
pid  ─────────────────────────┘                     └──────
st   ───────────────────────────────────────────────┘└───┘└─
173                        (o.factors_prod hx0)
id                          └────────────┘ └─┘
src  ─────────────────────┘ └────────────┘   └─
typ  ─────────────────────┘ └────────────┘└─┘└─
doc  ─────────────────────┘                  └─
txt  ─────────────────────┘                  └─
par  ─────────────────────┘                  └─
pid  ─────────────────────┘                  └─
st   ───────────────────────────────────────────
174                ... ~ᵤ (o.factors a).prod * (o.factors b).prod :
id                                              └───────┘
src  ─────────────────┘             └─────┘  └───────┘ └────────
typ  ─────────────────┘             └─────┘  └───────┘ └────────
doc  ─────────────────┘             └─────┘            └────────
txt  ─────────────────┘             └─────┘            └────────
par  ─────────────────┘             └─────┘            └────────
pid  ─────────────────┘             └─────┘            └────────
st   ─────────────┘└────────────────────────────────────────────────
175                  associated_mul_mul
id                   └────────────────┘
src  ───────────────┘└────────────────┘
typ  ───────────────┘└────────────────┘
doc  ───────────────┘                  
txt  ───────────────┘                  
par  ───────────────┘                  
pid  ───────────────┘                  
st   ───────────────────────────────────
176                    (o.factors_prod ha0).symm
src  ─────────────────┘                  └──────
typ  ─────────────────┘                  └──────
doc  ─────────────────┘                  └──────
txt  ─────────────────┘                  └──────
par  ─────────────────┘                  └──────
pid  ─────────────────┘                  └──────
st   ────────────────────────────────────────────
177                    (o.factors_prod hb0).symm
id                      └────────────┘
src  ─────────────────┘ └────────────┘   └──────
typ  ─────────────────┘ └────────────┘   └──────
doc  ─────────────────┘                  └──────
txt  ─────────────────┘                  └──────
par  ─────────────────┘                  └──────
pid  ─────────────────┘                  └──────
st   ────────────────────────────────────────────
178                ... = _ : by rw multiset.prod_add,
id                                 └───────────────┘
src  ─────────────────┘ └───┘  └─┘└───────────────┘└─
typ  ─────────────────┘ └───┘  └─┘└───────────────┘└─
doc  ─────────────────┘ └───┘  └─┘                 └─
txt  ─────────────────┘ └───┘  └─┘                 └─
par  ─────────────────┘ └───┘  └─┘                 └─
pid  ─────────────────┘ └───┘  └──┘                 └─
st   ─────────────────────────┘└───────────────────┘└─
179          let ⟨q, hqf, hq⟩ := multiset.exists_mem_of_rel_of_mem this
id                   └─┘  └┘     └───────────────────────────────┘
src  ───────┘     └┘   └┘  └───┘└───────────────────────────────┘    
typ  ───────┘     └┘└─┘└┘└┘└───┘└───────────────────────────────┘    
doc  ───────┘     └┘   └┘  └───┘                                     
txt  ───────┘     └┘   └┘  └───┘                                     
par  ───────┘     └┘   └┘  └───┘                                     
pid  ───────┘     └┘   └┘  └───┘                                     
st   ───────────────────────────────────────────────────────────────────
180            (multiset.mem_cons_self p _) in
id              └────────────────────┘
src  ─────────┘ └────────────────────┘ └──────
typ  ─────────┘ └────────────────────┘ └──────
doc  ─────────┘                        └──────
txt  ─────────┘                        └──────
par  ─────────┘                        └──────
pid  ─────────┘                        └──────
st   ──────────────────────────────────────────
181          (multiset.mem_add.1 hqf).elim
src  ───────┘                 └─┘   └──────
typ  ───────┘                 └─┘   └──────
doc  ───────┘                 └─┘   └──────
txt  ───────┘                 └─┘   └──────
par  ───────┘                 └─┘   └──────
pid  ───────┘                 └─┘   └──────
st   ──────────────────────────────────────
182            (λ hqa, or.inl $ (dvd_iff_dvd_of_rel_left hq).2 $
id                     └────┘
src  ─────────┘  └────┘└────┘                           └──┘ 
typ  ─────────┘  └────┘└────┘                           └──┘ 
doc  ─────────┘  └────┘                                 └──┘ 
txt  ─────────┘  └────┘                                 └──┘ 
par  ─────────┘  └────┘                                 └──┘ 
pid  ─────────┘  └────┘                                 └──┘ 
st   ────────────────────────────────────────────────────────────
183              (dvd_iff_dvd_of_rel_right (o.factors_prod ha0)).1
src  ───────────┘                                           └────
typ  ───────────┘                                           └────
doc  ───────────┘                                           └────
txt  ───────────┘                                           └────
par  ───────────┘                                           └────
pid  ───────────┘                                           └────
st   ──────────────────────────────────────────────────────────────
184                (multiset.dvd_prod hqa))
src  ─────────────┘                     └──
typ  ─────────────┘                     └──
doc  ─────────────┘                     └──
txt  ─────────────┘                     └──
par  ─────────────┘                     └──
pid  ─────────────┘                     └──
st   ───────────────────────────────────────
185            (λ hqb, or.inr $ (dvd_iff_dvd_of_rel_left hq).2 $
id                     └────┘    └─────────────────────┘
src  ─────────┘  └────┘└────┘  └─────────────────────┘  └──┘ 
typ  ─────────┘  └────┘└────┘  └─────────────────────┘  └──┘ 
doc  ─────────┘  └────┘                                 └──┘ 
txt  ─────────┘  └────┘                                 └──┘ 
par  ─────────┘  └────┘                                 └──┘ 
pid  ─────────┘  └────┘                                 └──┘ 
st   ────────────────────────────────────────────────────────────
186              (dvd_iff_dvd_of_rel_right (o.factors_prod hb0)).1
id                └──────────────────────┘
src  ───────────┘ └──────────────────────┘                  └────
typ  ───────────┘ └──────────────────────┘                  └────
doc  ───────────┘                                           └────
txt  ───────────┘                                           └────
par  ───────────┘                                           └────
pid  ───────────┘                                           └────
st   ──────────────────────────────────────────────────────────────
187                (multiset.dvd_prod hqb))⟩,
id                  └───────────────┘
src  ─────────────┘ └───────────────┘   └────
typ  ─────────────┘ └───────────────┘   └────
doc  ─────────────┘                     └────
txt  ─────────────┘                     └────
par  ─────────────┘                     └────
pid  ─────────────┘                     └────
st   ─────────────────────────────────────────
188    ..o }
id       
src  ───┘ └──
typ  ───┘└──
doc  ───┘ └──
txt  ───┘ └──
par  ───┘ └──
pid  ───┘ └┘
st   ────────
189  
src  
typ  
doc  
txt  
par  
pid  
st   
190  end unique_factorization_domain
191  
192  namespace associates
193  open unique_factorization_domain associated lattice
194  variables [integral_domain α] [unique_factorization_domain α] [decidable_eq (associates α)]
id              └─────────────┘     └─────────────────────────┘     └──────────┘  └────────┘
src             └─────────────┘     └─────────────────────────┘     └──────────┘  └────────┘
typ             └─────────────┘     └─────────────────────────┘     └──────────┘  └────────┘
doc                                 └─────────────────────────┘
195  
196  /-- `factor_set α` representation elements of unique factorization domain as multisets.
197  
198  `multiset α` produced by `factors` are only unique up to associated elements, while the multisets in
199  `factor_set α` are unqiue by equality and restricted to irreducible elements. This gives us a
200  representation of each element as a unique multisets (or the added ⊤ for 0), which has a complete
201  lattice struture. Infimum is the greatest common divisor and supremum is the least common multiple.
202  -/
203  @[reducible] def {u} factor_set (α : Type u) [integral_domain α] [unique_factorization_domain α] :
id                                                 └─────────────┘    └─────────────────────────┘ 
src                                                └─────────────┘     └─────────────────────────┘
typ                                                └─────────────┘    └─────────────────────────┘ 
doc    └───────┘                                                       └─────────────────────────┘
204    Type u :=
205  with_top (multiset { a : associates α // irreducible a })
id   └──────┘  └──────┘      └────────┘     └─────────┘ 
src  └──────┘  └──────┘      └────────┘      └─────────┘
typ  └──────┘  └──────┘      └────────┘     └─────────┘ 
doc            └──────┘                       └─────────┘
206  
207  local attribute [instance] associated.setoid
id                              └───────────────┘
src                             └───────────────┘
typ                             └───────────────┘
208  
209  theorem unique' {p q : multiset (associates α)} :
id                          └──────┘  └────────┘ 
src                         └──────┘  └────────┘
typ                         └──────┘  └────────┘ 
doc                         └──────┘
210    (∀a∈p, irreducible a) → (∀a∈q, irreducible a) → p.prod = q.prod → p = q :=
id          └─────────┘          └─────────┘     └───┘  └───┘     
src           └─────────┘             └─────────┘       └───┘   └───┘     
typ         └─────────┘          └─────────┘     └───┘  └───┘     
doc           └─────────┘             └─────────┘       └───┘    └───┘
211  begin
st   └─────
212    apply multiset.induction_on_multiset_quot p,
id           └─────────────────────────────────┘ 
src    └────┘└─────────────────────────────────┘
typ    └────┘└─────────────────────────────────┘
doc    └────┘                                   
txt    └────┘                                   
par    └────┘                                   
pid                                            
st   ────────────────────────────────────────────┘└─
213    apply multiset.induction_on_multiset_quot q,
id           └─────────────────────────────────┘ 
src    └────┘└─────────────────────────────────┘
typ    └────┘└─────────────────────────────────┘
doc    └────┘                                   
txt    └────┘                                   
par    └────┘                                   
pid                                            
st   ────────────────────────────────────────────┘└─
214    assume s t hs ht eq,
src    └─────────────────┘
typ    └─────────────────┘
doc    └─────────────────┘
txt    └─────────────────┘
par    └─────────────────┘
pid    └─────────────────┘
st   ────────────────────┘└─
215    refine multiset.map_mk_eq_map_mk_of_rel (unique_factorization_domain.unique _ _ _),
id            └──────────────────────────────┘  └────────────────────────────────┘
src    └─────┘└──────────────────────────────┘ └────────────────────────────────┘└─────┘
typ    └─────┘└──────────────────────────────┘ └────────────────────────────────┘└─────┘
doc    └─────┘                                                                   └─────┘
txt    └─────┘                                                                   └─────┘
par    └─────┘                                                                   └─────┘
pid                                                                             └─────┘
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
216    { exact assume a ha, ((irreducible_mk_iff _).1 $ hs _ $ multiset.mem_map_of_mem _ ha) },
id                            └────────────────┘        └┘     └─────────────────────┘
src      └────┘      └─────┘  └────────────────┘└────┘   └─┘ └─────────────────────┘└─┘  └┘
typ      └────┘      └─────┘  └────────────────┘└────┘ └┘└─┘ └─────────────────────┘└─┘  └┘
doc      └────┘      └─────┘                    └────┘   └─┘                        └─┘  └┘
txt      └────┘      └─────┘                    └────┘   └─┘                        └─┘  └┘
par      └────┘      └─────┘                    └────┘   └─┘                        └─┘  └┘
pid                 └─────┘                    └────┘   └─┘                        └─┘  
st   ───┘└──────────────────────────────────────────────────────────────────────────────────┘└┘
217    { exact assume a ha, ((irreducible_mk_iff _).1 $ ht _ $ multiset.mem_map_of_mem _ ha) },
id                            └────────────────┘        └┘     └─────────────────────┘
src      └────┘      └─────┘  └────────────────┘└────┘   └─┘ └─────────────────────┘└─┘  └┘
typ      └────┘      └─────┘  └────────────────┘└────┘ └┘└─┘ └─────────────────────┘└─┘  └┘
doc      └────┘      └─────┘                    └────┘   └─┘                        └─┘  └┘
txt      └────┘      └─────┘                    └────┘   └─┘                        └─┘  └┘
par      └────┘      └─────┘                    └────┘   └─┘                        └─┘  └┘
pid                 └─────┘                    └────┘   └─┘                        └─┘  
st   ───┘└──────────────────────────────────────────────────────────────────────────────────┘└┘
218    simpa [quot_mk_eq_mk, prod_mk, mk_eq_mk_iff_associated] using eq
id            └───────────┘  └─────┘  └─────────────────────┘        └┘
src    └─────┘└───────────┘└┘└─────┘└┘└─────────────────────┘└──────┘└┘
typ    └─────┘└───────────┘└┘└─────┘└┘└─────────────────────┘└──────┘└┘
doc    └─────┘             └┘       └┘                       └──────┘  
txt    └─────┘             └┘       └┘                       └──────┘  
par    └─────┘             └┘       └┘                       └──────┘  
pid                      └┘       └┘                       └────┘  
st   ──────────────────────────────────────────────────────────────────┘
219  end
st   └─┘
220  
221  private theorem forall_map_mk_factors_irreducible (x : α) (hx : x ≠ 0) :
id                                                                   
src                                                                    
typ                                                                  
222    ∀(a : associates α), a ∈ multiset.map associates.mk (factors x) → irreducible a :=
id           └────────┘      └──────────┘ └───────────┘  └─────┘     └─────────┘ 
src          └────────┘        └──────────┘ └───────────┘  └─────┘      └─────────┘
typ          └────────┘      └──────────┘ └───────────┘  └─────┘     └─────────┘ 
doc                             └──────────┘                             └─────────┘
223  begin
st   └─────
224    assume a ha,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
225    rcases multiset.mem_map.1 ha with ⟨c, hc, rfl⟩,
id            └──────────────┘   └┘
src    └─────┘└──────────────┘└─┘  └────────────────┘
typ    └─────┘└──────────────┘└─┘└┘└────────────────┘
doc    └─────┘                └─┘  └────────────────┘
txt    └─────┘                └─┘  └────────────────┘
par    └─────┘                └─┘  └────────────────┘
pid                          └─┘  └────────────────┘
st   ───────────────────────────────────────────────┘└─
226    exact (irreducible_mk_iff c).2 (irreducible_factors hx _ hc)
id            └────────────────┘      └─────────────────┘ └┘   └┘
src    └────┘ └────────────────┘ └──┘ └─────────────────┘  └─┘  └┘
typ    └────┘ └────────────────┘└──┘ └─────────────────┘└┘└─┘└┘└┘
doc    └────┘                    └──┘                      └─┘  └┘
txt    └────┘                    └──┘                      └─┘  └┘
par    └────┘                    └──┘                      └─┘  └┘
pid                             └──┘                      └─┘  
st   ──────────────────────────────────────────────────────────────┘
227  end
st   └─┘
228  
229  theorem prod_le_prod_iff_le {p q : multiset (associates α)}
id                                      └──────┘  └────────┘ 
src                                     └──────┘  └────────┘
typ                                     └──────┘  └────────┘ 
doc                                     └──────┘
230    (hp : ∀a∈p, irreducible a) (hq : ∀a∈q, irreducible a) :
id               └─────────┘             └─────────┘ 
src                └─────────┘                └─────────┘
typ              └─────────┘             └─────────┘ 
doc                └─────────┘                └─────────┘
231    p.prod ≤ q.prod ↔ p ≤ q :=
id     └───┘  └───┘    
src     └───┘   └───┘    
typ    └───┘  └───┘    
doc     └───┘    └───┘
232  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
233    begin
st     └─────
234      rintros ⟨⟨c⟩, eq⟩,
src      └───────────────┘
typ      └───────────────┘
doc      └───────────────┘
txt      └───────────────┘
par      └───────────────┘
pid             └────────┘
st   ────────────────────┘└─
235      have : c ≠ 0, from (mt mk_eq_zero_iff_eq_zero.2 $
id                         └┘ └────────────────────┘
src      └─────┘ └┘  └───┘ └┘└────────────────────┘└─┘ 
typ      └─────┘└┘  └───┘ └┘└────────────────────┘└─┘ 
doc      └─────┘  └┘  └───┘                         └─┘ 
txt      └─────┘  └┘  └───┘                         └─┘ 
par      └─────┘  └┘  └───┘                         └─┘ 
pid      └───┘└┘    └───┘                         └─┘ 
st   ───────────────┘└─────────────────────────────────────
236        assume (hc : quot.mk setoid.r c = 0),
id                      └─────┘ └──────┘  
src  ─────┘      └─────┘       └──────┘ └────
typ  ─────┘      └─────┘└─────┘└──────┘└────
doc  ─────┘      └─────┘                 └────
txt  ─────┘      └─────┘                 └────
par  ─────┘      └─────┘                 └────
pid  ─────┘      └─────┘                 └────
st   ────────────────────────────────────────────
237        have (0 : associates α) ∈ q, from prod_eq_zero_iff.1 $ eq ▸ hc.symm ▸ mul_zero _,
id                   └────────┘           └──────────────┘     └┘    └───┘   └──────┘
src  ─────┘     └──┘└────────┘ └┘ └─────┘└──────────────┘└─┘ └┘  └───┘ └──────┘└───
typ  ─────┘     └──┘└────────┘└┘└─────┘└──────────────┘└─┘ └┘  └───┘ └──────┘└───
doc  ─────┘     └──┘           └┘  └─────┘                └─┘                    └───
txt  ─────┘     └──┘           └┘  └─────┘                └─┘                    └───
par  ─────┘     └──┘           └┘  └─────┘                └─┘                    └───
pid  ─────┘     └──┘           └┘  └─────┘                └─┘                    └───
st   ────────────────────────────────────────────────────────────────────────────────────────
238        not_irreducible_zero ((irreducible_mk_iff 0).1 $ hq _ this)),
id         └──────────────────┘   └────────────────┘        └┘
src  ─────┘└──────────────────┘  └────────────────┘└────┘   └─┘    └┘
typ  ─────┘└──────────────────┘  └────────────────┘└────┘ └┘└─┘    └┘
doc  ─────┘                                        └────┘   └─┘    └┘
txt  ─────┘                                        └────┘   └─┘    └┘
par  ─────┘                                        └────┘   └─┘    └┘
pid  ─────┘                                        └────┘   └─┘    └┘
st   ─────────────────────────────────────────────────────────────────┘└─
239      have : associates.mk (factors c).prod = quot.mk setoid.r c,
id              └───────────┘  └─────┘           └─────┘ └──────┘ 
src      └─────┘└───────────┘ └─────┘ └─────┘        └──────┘
typ      └─────┘└───────────┘ └─────┘ └─────┘ └─────┘└──────┘
doc      └─────┘                      └─────┘                
txt      └─────┘                      └─────┘                
par      └─────┘                      └─────┘                
pid      └───┘└┘                      └─────┘                
st   ─────────────────────────────────────────────────────────────┘└─
240        from mk_eq_mk_iff_associated.2 (factors_prod this),
id              └─────────────────────┘    └──────────┘ └──┘
src        └───┘└─────────────────────┘└─┘ └──────────┘    
typ        └───┘└─────────────────────┘└─┘ └──────────┘└──┘
doc        └───┘                       └─┘                 
txt        └───┘                       └─┘                 
par        └───┘                       └─┘                 
pid        └───┘                       └─┘                 
st   ───────────────────────────────────────────────────────┘└─
241  
st   
242      refine le_iff_exists_add.2 ⟨(factors c).map associates.mk, unique' hq _ _⟩,
id              └───────────────┘     └─────┘       └───────────┘  └─────┘ └┘
src      └─────┘└───────────────┘└─┘  └─────┘ └────┘└───────────┘└┘└─────┘  └───┘
typ      └─────┘└───────────────┘└─┘  └─────┘└────┘└───────────┘└┘└─────┘└┘└───┘
doc      └─────┘                 └─┘          └────┘             └┘         └───┘
txt      └─────┘                 └─┘          └────┘             └┘         └───┘
par      └─────┘                 └─┘          └────┘             └┘         └───┘
pid                             └─┘          └────┘             └┘         └───┘
st   ─────────────────────────────────────────────────────────────────────────────┘└─
243      { assume x hx,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid        └─────────┘
st   ─────┘└─────────┘└─
244        rcases multiset.mem_add.1 hx with h | h,
id                └──────────────┘   └┘
src        └─────┘└──────────────┘└─┘  └─────────┘
typ        └─────┘└──────────────┘└─┘└┘└─────────┘
doc        └─────┘                └─┘  └─────────┘
txt        └─────┘                └─┘  └─────────┘
par        └─────┘                └─┘  └─────────┘
pid                              └─┘  └─────────┘
st   ────────────────────────────────────────────┘└─
245        exact hp x h,
id               └┘  
src        └────┘   
typ        └────┘└┘
doc        └────┘   
txt        └────┘   
par        └────┘   
pid                
st   ─────────────────┘└─
246        exact forall_map_mk_factors_irreducible c ‹c ≠ 0› _ h },
id               └───────────────────────────────┘          
src        └────┘└───────────────────────────────┘   └┘└─┘ 
typ        └────┘└───────────────────────────────┘  └┘└─┘
doc        └────┘                                    └┘└─┘ 
txt        └────┘                                     └┘ └─┘ 
par        └────┘                                     └┘ └─┘ 
pid                                                  └┘ └─┘ 
st   ───────────────────────────────────────────────────────────┘└┘
247      { simp [multiset.prod_add, prod_mk, *] at * }
id               └───────────────┘  └─────┘
src        └────┘└───────────────┘└┘└─────┘└────────┘
typ        └────┘└───────────────┘└┘└─────┘└────────┘
doc        └────┘                 └┘       └────────┘
txt        └────┘                 └┘       └────────┘
par        └────┘                 └┘       └────────┘
pid                             └┘       └──┘└──┘
st   ───────────────────────────────────────────────┘└─
248    end
st   ────┘
249    prod_le_prod
id     └──────────┘
src    └──────────┘
typ    └──────────┘
250  
251  @[simp] theorem factor_set.coe_add {a b : multiset { a : associates α // irreducible a }} :
id                                             └──────┘      └────────┘     └─────────┘ 
src                                            └──────┘      └────────┘      └─────────┘
typ                                            └──────┘      └────────┘     └─────────┘ 
doc    └──┘                                    └──────┘                       └─────────┘
252    (↑a + ↑b : factor_set α) = ↑(a + b) :=
id           └────────┘       
src            └────────┘        
typ          └────────┘       
doc               └────────┘
253  with_top.coe_add
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
254  
255  lemma factor_set.sup_add_inf_eq_add : ∀(a b : factor_set α), a ⊔ b + a ⊓ b = a + b
id                                                └────────┘              
src                                                └────────┘                   
typ                                               └────────┘              
doc                                                └────────┘
256  | none     b        := show ⊤ ⊔ b + ⊤ ⊓ b = ⊤ + b, by simp
id     └──┘                                
src    └──┘                                        └───┘
typ    └──┘                                       └───┘
doc                                                        └───┘
txt                                                        └───┘
par                                                        └───┘
pid                                                            
st                                                        └────┘
257  | a        none     := show a ⊔ ⊤ + a ⊓ ⊤ = a + ⊤, by simp
id             └──┘                          
src             └──┘                               └───┘
typ            └──┘                               └───┘
doc                                                        └───┘
txt                                                        └───┘
par                                                        └───┘
pid                                                            
st                                                        └────┘
258  | (some a) (some b) := show (a : factor_set α) ⊔ b + a ⊓ b = a + b, from
id              └──┘                └────────┘               
src              └──┘                 └────────┘                
typ             └──┘                └────────┘               
doc                                   └────────┘
259    begin
st     └─────
260      rw [← with_top.coe_sup, ← with_top.coe_inf, ← with_top.coe_add, ← with_top.coe_add,
id             └──────────────┘    └──────────────┘    └──────────────┘    └──────────────┘
src      └────┘└──────────────┘└──┘└──────────────┘└──┘└──────────────┘└──┘└──────────────┘└─
typ      └────┘└──────────────┘└──┘└──────────────┘└──┘└──────────────┘└──┘└──────────────┘└─
doc      └────┘                └──┘                └──┘                └──┘                └─
txt      └────┘                └──┘                └──┘                └──┘                └─
par      └────┘                └──┘                └──┘                └──┘                └─
pid        └──┘                └──┘                └──┘                └──┘                └─
st   ─────────────────────────┘└──────────────────┘└──────────────────┘└──────────────────┘└─
261        with_top.coe_eq_coe],
id         └─────────────────┘
src  ─────┘└─────────────────┘
typ  ─────┘└─────────────────┘
doc  ─────┘                   
txt  ─────┘                   
par  ─────┘                   
pid  ─────┘                   
st   ────────────────────────┘└──
262      exact multiset.union_add_inter _ _
id             └──────────────────────┘
src      └────┘└──────────────────────┘└────
typ      └────┘└──────────────────────┘└────
doc      └────┘                        └────
txt      └────┘                        └────
par      └────┘                        └────
pid                                   └──┘
st   ───────────────────────────────────────
263    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
264  
265  def factors' (a : α) (ha : a ≠ 0) : multiset { a : associates α // irreducible a } :=
id                                    └──────┘      └────────┘     └─────────┘ 
src                                     └──────┘      └────────┘      └─────────┘
typ                                   └──────┘      └────────┘     └─────────┘ 
doc                                      └──────┘                       └─────────┘
266  (factors a).pmap (λa ha, ⟨associates.mk a, (irreducible_mk_iff _).2 ha⟩)
id    └─────┘  └──┘     └┘   └───────────┘    └────────────────┘     └┘
src   └─────┘   └──┘           └───────────┘     └────────────────┘   
typ   └─────┘  └──┘     └┘   └───────────┘    └────────────────┘     └┘
doc             └──┘
267    (irreducible_factors $ ha)
id      └─────────────────┘   └┘
src     └─────────────────┘
typ     └─────────────────┘   └┘
268  
269  @[simp] theorem map_subtype_val_factors' {a : α} (ha : a ≠ 0) :
id                                                          
src                                                           
typ                                                         
doc    └──┘
270    (factors' a ha).map subtype.val = (factors a).map associates.mk :=
id      └──────┘  └┘ └─┘  └─────────┘   └─────┘  └─┘  └───────────┘
src     └──────┘      └─┘  └─────────┘   └─────┘   └─┘  └───────────┘
typ     └──────┘  └┘ └─┘  └─────────┘   └─────┘  └─┘  └───────────┘
doc                   └─┘                           └─┘
271  by simp [factors', multiset.map_pmap, multiset.pmap_eq_map]
id            └──────┘  └───────────────┘  └──────────────────┘
src     └────┘└──────┘└┘└───────────────┘└┘└──────────────────┘└─
typ     └────┘└──────┘└┘└───────────────┘└┘└──────────────────┘└─
doc     └────┘        └┘                 └┘                    └─
txt     └────┘        └┘                 └┘                    └─
par     └────┘        └┘                 └┘                    └─
pid                 └┘                 └┘                    
st     └─────────────────────────────────────────────────────────
272  
src  
typ  
doc  
txt  
par  
pid  
st   
273  theorem factors'_cong {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) (h : a ~ᵤ b) :
id                                                              └┘ 
src                                                                 └┘
typ                                                             └┘ 
274    factors' a ha = factors' b hb :=
id     └──────┘  └┘  └──────┘  └┘
src    └──────┘       └──────┘
typ    └──────┘  └┘  └──────┘  └┘
275  have multiset.rel associated (factors a) (factors b), from
id        └──────────┘ └────────┘  └─────┘    └─────┘ 
src       └──────────┘ └────────┘  └─────┘     └─────┘
typ       └──────────┘ └────────┘  └─────┘    └─────┘ 
doc       └──────────┘
276    unique (irreducible_factors ha) (irreducible_factors hb)
id     └────┘  └─────────────────┘ └┘   └─────────────────┘ └┘
src    └────┘  └─────────────────┘      └─────────────────┘
typ    └────┘  └─────────────────┘ └┘   └─────────────────┘ └┘
277      ((factors_prod ha).trans $ h.trans $ (factors_prod hb).symm),
id         └──────────┘ └┘ └───┘    └────┘    └──────────┘ └┘ └──┘
src        └──────────┘    └───┘     └────┘    └──────────┘    └──┘
typ        └──────────┘ └┘ └───┘    └────┘    └──────────┘ └┘ └──┘
278  by simpa [(multiset.map_eq_map subtype.val_injective).symm, rel_associated_iff_map_eq_map.symm]
id              └─────────────────┘ └───────────────────┘
src     └─────┘ └─────────────────┘└───────────────────┘└──────┘                                  └─
typ     └─────┘ └─────────────────┘└───────────────────┘└──────┘└────────────────────────────────┘└─
doc     └─────┘                                         └──────┘                                  └─
txt     └─────┘                                         └──────┘                                  └─
par     └─────┘                                         └──────┘                                  └─
pid                                                   └──────┘                                  
st     └─────────────────────────────────────────────────────────────────────────────────────────────
279  
src  
typ  
doc  
txt  
par  
pid  
st   
280  def factors (a : associates α) : factor_set α :=
id                    └────────┘     └────────┘ 
src                   └────────┘      └────────┘
typ                   └────────┘     └────────┘ 
doc                                   └────────┘
281  begin
st   └─────
282    refine (if h : a = 0 then ⊤ else
id             └┘               
src    └─────┘ └┘└───┘ └──────┘└─────
typ    └─────┘ └┘└───┘ └──────┘└─────
doc    └─────┘   └───┘  └──────┘ └─────
txt    └─────┘   └───┘  └──────┘ └─────
par    └─────┘   └───┘  └──────┘ └─────
pid             └───┘  └──────┘ └─────
st   ───────────────────────────────────
283      quotient.hrec_on a (λx h, some $ factors' x (mt mk_eq_zero_iff_eq_zero.2 h)) _ h),
id       └──────────────┘         └──┘   └──────┘    └┘ └────────────────────┘
src  ───┘└──────────────┘   └───┘└──┘ └──────┘  └┘└────────────────────┘└─┘ └───┘ 
typ  ───┘└──────────────┘  └───┘└──┘ └──────┘  └┘└────────────────────┘└─┘ └───┘ 
doc  ───┘                   └───┘                                       └─┘ └───┘ 
txt  ───┘                   └───┘                                       └─┘ └───┘ 
par  ───┘                   └───┘                                       └─┘ └───┘ 
pid  ───┘                   └───┘                                       └─┘ └───┘ 
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
284  
st   
285    assume a b hab,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid    └────────────┘
st   ───────────────┘└─
286    apply function.hfunext,
id           └──────────────┘
src    └────┘└──────────────┘
typ    └────┘└──────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────────┘└─
287    { have : a ~ᵤ 0 ↔ b ~ᵤ 0, from
id               └┘     
src      └─────┘ └┘└─┘    └┘  └────
typ      └─────┘└┘└─┘   └┘  └────
doc      └─────┘   └─┘    └┘  └────
txt      └─────┘   └─┘    └┘  └────
par      └─────┘   └─┘    └┘  └────
pid      └───┘└┘   └─┘      └────
st   ───┘└────────────────────┘└──────
288        iff.intro (assume ha0, hab.symm.trans ha0) (assume hb0, hab.trans hb0),
id         └───────┘              └────────────┘                   └───────┘
src  ─────┘└───────┘       └────┘└────────────┘   └┘       └────┘└───────┘   
typ  ─────┘└───────┘       └────┘└────────────┘   └┘       └────┘└───────┘   
doc  ─────┘                └────┘                 └┘       └────┘            
txt  ─────┘                └────┘                 └┘       └────┘            
par  ─────┘                └────┘                 └┘       └────┘            
pid  ─────┘                └────┘                 └┘       └────┘            
st   ───────────────────────────────────────────────────────────────────────────┘└─
289      simp [quotient_mk_eq_mk, mk_eq_zero_iff_eq_zero, (associated_zero_iff_eq_zero _).symm, this] },
id             └───────────────┘  └────────────────────┘   └─────────────────────────┘          └──┘
src      └────┘└───────────────┘└┘└────────────────────┘└┘ └─────────────────────────┘└────────┘    └┘
typ      └────┘└───────────────┘└┘└────────────────────┘└┘ └─────────────────────────┘└────────┘└──┘└┘
doc      └────┘                 └┘                      └┘                            └────────┘    └┘
txt      └────┘                 └┘                      └┘                            └────────┘    └┘
par      └────┘                 └┘                      └┘                            └────────┘    └┘
pid                           └┘                      └┘                            └────────┘    
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└┘
290    exact (assume ha hb eq, heq_of_eq $ congr_arg some $ factors'_cong _ _ hab)
id                             └───────┘   └───────┘ └──┘   └───────────┘     └─┘
src    └────┘       └─────────┘└───────┘ └───────┘└──┘ └───────────┘└───┘   └┘
typ    └────┘       └─────────┘└───────┘ └───────┘└──┘ └───────────┘└───┘└─┘└┘
doc    └────┘       └─────────┘                                     └───┘   └┘
txt    └────┘       └─────────┘                                     └───┘   └┘
par    └────┘       └─────────┘                                     └───┘   └┘
pid                └─────────┘                                     └───┘   
st   ─────────────────────────────────────────────────────────────────────────────┘
291  end
st   └─┘
292  
293  @[simp] theorem factors_0 : (0 : associates α).factors = ⊤ :=
id                                    └────────┘  └─────┘   
src                                   └────────┘   └─────┘   
typ                                   └────────┘  └─────┘   
doc    └──┘
294  dif_pos rfl
id   └─────┘ └─┘
src  └─────┘ └─┘
typ  └─────┘ └─┘
295  
296  @[simp] theorem factors_mk (a : α) (h : a ≠ 0) : (associates.mk a).factors = factors' a h :=
id                                                  └───────────┘  └─────┘   └──────┘  
src                                                   └───────────┘   └─────┘   └──────┘
typ                                                 └───────────┘  └─────┘   └──────┘  
doc    └──┘
297  dif_neg (mt mk_eq_zero_iff_eq_zero.1 h)
id   └─────┘  └┘ └────────────────────┘  
src  └─────┘  └┘ └────────────────────┘
typ  └─────┘  └┘ └────────────────────┘  
298  
299  def factor_set.prod : factor_set α → associates α
id                         └────────┘   └────────┘ 
src                        └────────┘     └────────┘
typ                        └────────┘   └────────┘ 
doc                        └────────┘
300  | none     := 0
id     └──┘
src    └──┘
typ    └──┘
301  | (some s) := (s.map subtype.val).prod
id      └──┘        └──┘ └─────────┘ └──┘
src     └──┘         └──┘ └─────────┘ └──┘
typ     └──┘        └──┘ └─────────┘ └──┘
doc                  └──┘             └──┘
302  
303  @[simp] theorem prod_top : (⊤ : factor_set α).prod = 0 := rfl
id                                  └────────┘  └──┘        └─┘
src                                 └────────┘   └──┘        └─┘
typ                                 └────────┘  └──┘        └─┘
doc    └──┘                          └────────┘
304  
305  @[simp] theorem prod_coe {s : multiset { a : associates α // irreducible a }} :
id                                 └──────┘      └────────┘     └─────────┘ 
src                                └──────┘      └────────┘      └─────────┘
typ                                └──────┘      └────────┘     └─────────┘ 
doc    └──┘                        └──────┘                       └─────────┘
306    (s : factor_set α).prod = (s.map subtype.val).prod :=
id         └────────┘  └──┘    └──┘ └─────────┘ └──┘
src         └────────┘   └──┘     └──┘ └─────────┘ └──┘
typ        └────────┘  └──┘    └──┘ └─────────┘ └──┘
doc         └────────┘             └──┘             └──┘
307  rfl
id   └─┘
src  └─┘
typ  └─┘
308  
309  theorem prod_factors : ∀(s : factor_set α), s.prod.factors = s
id                               └────────┘    └───┘└──────┘  
src                               └────────┘      └───┘└──────┘ 
typ                              └────────┘    └───┘└──────┘  
doc                               └────────┘
310  | none     := by simp [factor_set.prod]; refl
id     └──┘                 └─────────────┘
src    └──┘           └────┘└─────────────┘  └───┘
typ    └──┘           └────┘└─────────────┘  └───┘
doc                   └────┘                 └───┘
txt                   └────┘                 └───┘
par                   └────┘                 └───┘
pid                                            
st                   └────────────────────────────┘
311  | (some s) :=
id      └──┘
src     └──┘
typ     └──┘
312    begin
st     └─────
313      unfold factor_set.prod,
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid            └──────────────┘
st   ─────────────────────────┘└─
314      generalize eq_a : (s.map subtype.val).prod = a,
id                          └───┘ └─────────┘
src      └────────────────┘ └───┘└─────────┘└─────┘ 
typ      └────────────────┘ └───┘└─────────┘└─────┘ 
doc      └────────────────┘ └───┘           └─────┘ 
txt      └────────────────┘                 └─────┘ 
par      └────────────────┘                 └─────┘ 
pid                └───┘└┘                 └─────┘ 
st   ─────────────────────────────────────────────────┘└─
315      rcases a with ⟨a⟩,
id              
src      └─────┘ └───────┘
typ      └─────┘└───────┘
doc      └─────┘ └───────┘
txt      └─────┘ └───────┘
par      └─────┘ └───────┘
pid             └───────┘
st   ────────────────────┘└─
316      rw quot_mk_eq_mk at *,
id          └───────────┘
src      └─┘└───────────┘└───┘
typ      └─┘└───────────┘└───┘
doc      └─┘             └───┘
txt      └─┘             └───┘
par      └─┘             └───┘
pid                     └───┘
st   ────────────────────────┘└─
317  
st   
318      have : (s.map subtype.val).prod ≠ 0, from assume ha,
id               └───┘ └─────────┘       
src      └─────┘ └───┘└─────────┘└─────┘└┘  └───┘      └────
typ      └─────┘ └───┘└─────────┘└─────┘└┘  └───┘      └────
doc      └─────┘ └───┘           └─────┘ └┘  └───┘      └────
txt      └─────┘                 └─────┘ └┘  └───┘      └────
par      └─────┘                 └─────┘ └┘  └───┘      └────
pid      └───┘└┘                 └─────┘   └───┘      └────
st   ──────────────────────────────────────┘└─────────────────
319        let ⟨⟨a, ha⟩, h, eq⟩ := multiset.mem_map.1 (prod_eq_zero_iff.1 ha) in
id                          └┘     └──────────────┘    └──────────────┘
src  ─────┘      └┘  └─┘ └┘└┘└───┘└──────────────┘└─┘ └──────────────┘└─┘  └────
typ  ─────┘      └┘  └─┘ └┘└┘└───┘└──────────────┘└─┘ └──────────────┘└─┘  └────
doc  ─────┘      └┘  └─┘ └┘  └───┘                └─┘                 └─┘  └────
txt  ─────┘      └┘  └─┘ └┘  └───┘                └─┘                 └─┘  └────
par  ─────┘      └┘  └─┘ └┘  └───┘                └─┘                 └─┘  └────
pid  ─────┘      └┘  └─┘ └┘  └───┘                └─┘                 └─┘  └────
st   ────────────────────────────────────────────────────────────────────────────
320        have irreducible (0 : associates α), from eq ▸ ha,
id                               └────────┘            
src  ─────┘    └───────────┘ └──┘└────────┘ └──────┘    └─
typ  ─────┘    └───────────┘ └──┘└────────┘└──────┘    └─
doc  ─────┘    └───────────┘ └──┘           └──────┘     └─
txt  ─────┘    └───────────┘ └──┘           └──────┘     └─
par  ─────┘    └───────────┘ └──┘           └──────┘     └─
pid  ─────┘    └───────────┘ └──┘           └──────┘     └─
st   ─────────────────────────────────────────────────────────
321        not_irreducible_zero ((irreducible_mk_iff _).1 this),
id         └──────────────────┘   └────────────────┘
src  ─────┘└──────────────────┘  └────────────────┘└────┘    
typ  ─────┘└──────────────────┘  └────────────────┘└────┘    
doc  ─────┘                                        └────┘    
txt  ─────┘                                        └────┘    
par  ─────┘                                        └────┘    
pid  ─────┘                                        └────┘    
st   ─────────────────────────────────────────────────────────┘└─
322      have ha : a ≠ 0, by simp [*] at *,
id                 
src      └────────┘  └┘     └───────────┘
typ      └────────┘ └┘     └───────────┘
doc      └────────┘  └┘     └───────────┘
txt      └────────┘  └┘     └───────────┘
par      └────────┘  └┘     └───────────┘
pid      └─────┘└─┘           └─┘└──┘
st   ──────────────────┘                  └─
323      suffices : (unique_factorization_domain.factors a).map associates.mk = s.map subtype.val,
id                   └─────────────────────────────────┘       └───────────┘   └───┘ └─────────┘
src      └─────────┘ └─────────────────────────────────┘ └────┘└───────────┘ └───┘└─────────┘
typ      └─────────┘ └─────────────────────────────────┘└────┘└───────────┘ └───┘└─────────┘
doc      └─────────┘                                     └────┘              └───┘
txt      └─────────┘                                     └────┘                   
par      └─────────┘                                     └────┘                   
pid      └───────┘└┘                                     └────┘                   
st   ───────────────────────────────────────────────────────────────────────────────────────────┘└─
324      { rw [factors_mk a ha],
id             └────────┘  └┘
src        └──┘└────────┘   
typ        └──┘└────────┘└┘
doc        └──┘             
txt        └──┘             
par        └──┘             
pid          └┘             
st   ─────┘└─────────────────┘└──
325        apply congr_arg some _,
id               └───────┘ └──┘
src        └────┘└───────┘└──┘└┘
typ        └────┘└───────┘└──┘└┘
doc        └────┘             └┘
txt        └────┘             └┘
par        └────┘             └┘
pid                          └┘
st   ───────────────────────────┘└─
326        simpa [(multiset.map_eq_map subtype.val_injective).symm] },
id                 └─────────────────┘ └───────────────────┘
src        └─────┘ └─────────────────┘└───────────────────┘└──────┘
typ        └─────┘ └─────────────────┘└───────────────────┘└──────┘
doc        └─────┘                                         └──────┘
txt        └─────┘                                         └──────┘
par        └─────┘                                         └──────┘
pid                                                      └─────┘
st   ──────────────────────────────────────────────────────────────┘└┘
327  
st   
328      refine unique'
id              └─────┘
src      └─────┘└─────┘
typ      └─────┘└─────┘
doc      └─────┘       
txt      └─────┘       
par      └─────┘       
pid                   
st   ───────────────────
329        (forall_map_mk_factors_irreducible _ ha)
id          └───────────────────────────────┘   └┘
src  ─────┘ └───────────────────────────────┘└─┘  └─
typ  ─────┘ └───────────────────────────────┘└─┘└┘└─
doc  ─────┘                                  └─┘  └─
txt  ─────┘                                  └─┘  └─
par  ─────┘                                  └─┘  └─
pid  ─────┘                                  └─┘  └─
st   ───────────────────────────────────────────────
330        (assume a ha, let ⟨⟨x, hx⟩, ha, eq⟩ := multiset.mem_map.1 ha in eq ▸ hx)
id                                └┘       └┘     └──────────────┘
src  ─────┘       └─────┘      └┘  └─┘  └┘└┘└───┘└──────────────┘└─┘  └──┘     └─
typ  ─────┘       └─────┘      └┘└┘└─┘  └┘└┘└───┘└──────────────┘└─┘  └──┘     └─
doc  ─────┘       └─────┘      └┘  └─┘  └┘  └───┘                └─┘  └──┘     └─
txt  ─────┘       └─────┘      └┘  └─┘  └┘  └───┘                └─┘  └──┘     └─
par  ─────┘       └─────┘      └┘  └─┘  └┘  └───┘                └─┘  └──┘     └─
pid  ─────┘       └─────┘      └┘  └─┘  └┘  └───┘                └─┘  └──┘     └─
st   ───────────────────────────────────────────────────────────────────────────────
331        _,
src  ──────┘
typ  ──────┘
doc  ──────┘
txt  ──────┘
par  ──────┘
pid  ──────┘
st   ──────┘└─
332      rw [prod_mk, eq_a, mk_eq_mk_iff_associated],
id           └─────┘  └──┘  └─────────────────────┘
src      └──┘└─────┘└┘    └┘└─────────────────────┘
typ      └──┘└─────┘└┘└──┘└┘└─────────────────────┘
doc      └──┘       └┘    └┘                       
txt      └──┘       └┘    └┘                       
par      └──┘       └┘    └┘                       
pid        └┘       └┘    └┘                       
st   ──────────────┘└────┘└───────────────────────┘└──
333      exact factors_prod ha
id             └──────────┘ └┘
src      └────┘└──────────┘  
typ      └────┘└──────────┘└┘
doc      └────┘              
txt      └────┘              
par      └────┘              
pid                         
st   ──────────────────────────
334    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
335  
336  theorem factors_prod (a : associates α) : a.factors.prod = a :=
id                             └────────┘     └──────┘└───┘  
src                            └────────┘       └──────┘└───┘ 
typ                            └────────┘     └──────┘└───┘  
337  quotient.induction_on a $ assume a, decidable.by_cases
id   └───────────────────┘             └────────────────┘
src  └───────────────────┘               └────────────────┘
typ  └───────────────────┘             └────────────────┘
338    (assume : associates.mk a = 0, by simp [quotient_mk_eq_mk, this])
id               └───────────┘               └───────────────┘  └──┘
src              └───────────┘          └────┘└───────────────┘└┘    
typ              └───────────┘         └────┘└───────────────┘└┘└──┘
doc                                      └────┘                 └┘    
txt                                      └────┘                 └┘    
par                                      └────┘                 └┘    
pid                                                           └┘    
st                                      └─────────────────────────────┘
339    (assume : associates.mk a ≠ 0,
id               └───────────┘  
src              └───────────┘   
typ              └───────────┘  
340      have a ≠ 0, by simp * at *,
id             
src                    └─────────┘
typ                   └─────────┘
doc                     └─────────┘
txt                     └─────────┘
par                     └─────────┘
pid                         └──┘
st                     └──────────┘
341      by simp [this, quotient_mk_eq_mk, prod_mk, mk_eq_mk_iff_associated.2 (factors_prod this)])
id                └──┘  └───────────────┘  └─────┘  └─────────────────────┘    └──────────┘ └──┘
src         └────┘    └┘└───────────────┘└┘└─────┘└┘└─────────────────────┘└─┘ └──────────┘    └┘
typ         └────┘└──┘└┘└───────────────┘└┘└─────┘└┘└─────────────────────┘└─┘ └──────────┘└──┘└┘
doc         └────┘    └┘                 └┘       └┘                       └─┘                 └┘
txt         └────┘    └┘                 └┘       └┘                       └─┘                 └┘
par         └────┘    └┘                 └┘       └┘                       └─┘                 └┘
pid                 └┘                 └┘       └┘                       └─┘                 └┘
st         └─────────────────────────────────────────────────────────────────────────────────────┘
342  
343  theorem eq_of_factors_eq_factors {a b : associates α} (h : a.factors = b.factors) : a = b :=
id                                           └────────┘        └──────┘  └──────┘      
src                                          └────────┘          └──────┘   └──────┘      
typ                                          └────────┘        └──────┘  └──────┘      
344  have a.factors.prod = b.factors.prod, by rw h,
id        └──────┘└───┘  └──────┘└───┘        
src        └──────┘└───┘   └──────┘└───┘     └─┘
typ       └──────┘└───┘  └──────┘└───┘     └─┘
doc                                           └─┘
txt                                           └─┘
par                                           └─┘
pid                                             
st                                           └───┘
345  by rwa [factors_prod, factors_prod] at this
id           └──────────┘  └──────────┘
src     └───┘└──────────┘└┘└──────────┘└─────────
typ     └───┘└──────────┘└┘└──────────┘└─────────
doc     └───┘            └┘            └─────────
txt     └───┘            └┘            └─────────
par     └───┘            └┘            └─────────
pid        └┘            └┘            └──────┘
st     └────────────────┘└────────────┘└────────
346  
src  
typ  
doc  
txt  
par  
pid  
st   
347  theorem eq_of_prod_eq_prod {a b : factor_set α} (h : a.prod = b.prod) : a = b :=
id                                     └────────┘        └───┘  └───┘      
src                                    └────────┘          └───┘   └───┘      
typ                                    └────────┘        └───┘  └───┘      
doc                                    └────────┘
348  have a.prod.factors = b.prod.factors, by rw h,
id        └───┘└──────┘  └───┘└──────┘        
src        └───┘└──────┘   └───┘└──────┘     └─┘
typ       └───┘└──────┘  └───┘└──────┘     └─┘
doc                                           └─┘
txt                                           └─┘
par                                           └─┘
pid                                             
st                                           └───┘
349  by rwa [prod_factors, prod_factors] at this
id           └──────────┘  └──────────┘
src     └───┘└──────────┘└┘└──────────┘└─────────
typ     └───┘└──────────┘└┘└──────────┘└─────────
doc     └───┘            └┘            └─────────
txt     └───┘            └┘            └─────────
par     └───┘            └┘            └─────────
pid        └┘            └┘            └──────┘
st     └────────────────┘└────────────┘└────────
350  
src  
typ  
doc  
txt  
par  
pid  
st   
351  @[simp] theorem prod_add : ∀(a b : factor_set α), (a + b).prod = a.prod * b.prod
id                                     └────────┘        └──┘   └───┘  └───┘
src                                     └────────┘           └──┘    └───┘   └───┘
typ                                    └────────┘        └──┘   └───┘  └───┘
doc    └──┘                             └────────┘
352  | none b    := show (⊤ + b).prod = (⊤:factor_set α).prod * b.prod, by simp
id     └──┘                  └──┘     └────────┘  └──┘    └───┘
src    └──┘                   └──┘     └────────┘   └──┘    └───┘     └───┘
typ    └──┘                  └──┘     └────────┘  └──┘    └───┘     └───┘
doc                                        └────────┘                      └───┘
txt                                                                        └───┘
par                                                                        └───┘
pid                                                                            
st                                                                        └────┘
353  | a    none := show (a + ⊤).prod = a.prod * (⊤:factor_set α).prod, by simp
id         └──┘              └──┘    └───┘    └────────┘  └──┘
src         └──┘              └──┘    └───┘    └────────┘   └──┘      └───┘
typ        └──┘              └──┘    └───┘    └────────┘  └──┘      └───┘
doc                                                 └────────┘             └───┘
txt                                                                        └───┘
par                                                                        └───┘
pid                                                                            
st                                                                        └────┘
354  | (some a) (some b) :=
id              └──┘ 
src              └──┘
typ             └──┘ 
355    show (↑a + ↑b:factor_set α).prod = (↑a:factor_set α).prod * (↑b:factor_set α).prod,
id                └────────┘  └──┘      └────────┘  └──┘      └────────┘  └──┘
src               └────────┘   └──┘      └────────┘   └──┘      └────────┘   └──┘
typ               └────────┘  └──┘      └────────┘  └──┘      └────────┘  └──┘
doc                  └────────┘               └────────┘               └────────┘
356      by rw [factor_set.coe_add, prod_coe, prod_coe, prod_coe, multiset.map_add, multiset.prod_add]
id              └────────────────┘  └──────┘  └──────┘  └──────┘  └──────────────┘  └───────────────┘
src         └──┘└────────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└──────────────┘└┘└───────────────┘└─
typ         └──┘└────────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└──────────────┘└┘└───────────────┘└─
doc         └──┘                  └┘        └┘        └┘        └┘                └┘                 └─
txt         └──┘                  └┘        └┘        └┘        └┘                └┘                 └─
par         └──┘                  └┘        └┘        └┘        └┘                └┘                 └─
pid           └┘                  └┘        └┘        └┘        └┘                └┘                 
st         └─────────────────────┘└────────┘└────────┘└────────┘└────────────────┘└─────────────────┘
357  
src  
typ  
doc  
txt  
par  
pid  
st   
358  theorem prod_mono : ∀{a b : factor_set α}, a ≤ b → a.prod ≤ b.prod
id                              └────────┘         └───┘  └───┘
src                              └────────┘             └───┘   └───┘
typ                             └────────┘         └───┘  └───┘
doc                              └────────┘
359  | none b h := have b = ⊤, from top_unique h, by rw [this, prod_top]; exact le_refl _
id     └──┘                     └────────┘           └──┘  └──────┘         └─────┘
src    └──┘                       └────────┘       └──┘    └┘└──────┘  └────┘└─────┘└─┘
typ    └──┘                     └────────┘       └──┘└──┘└┘└──────┘  └────┘└─────┘└─┘
doc                                                  └──┘    └┘          └────┘       └─┘
txt                                                  └──┘    └┘          └────┘       └─┘
par                                                  └──┘    └┘          └────┘       └─┘
pid                                                    └┘    └┘                      └┘
st                                                  └───────┘└────────┘└────────────────┘
360  | a none h := show a.prod ≤ (⊤ : factor_set α).prod, by simp; exact le_top
id      └──┘            └───┘      └────────┘  └──┘                  └────┘
src      └──┘            └───┘      └────────┘   └──┘      └──┘  └────┘└────┘
typ     └──┘            └───┘      └────────┘  └──┘      └──┘  └────┘└────┘
doc                                   └────────┘             └──┘  └────┘      
txt                                                          └──┘  └────┘      
par                                                          └──┘  └────┘      
pid                                                                           
st                                                          └──────────────────┘
361  | (some a) (some b) h := prod_le_prod $ multiset.map_le_map $ with_top.coe_le_coe.1 $ h
id               └──┘        └──────────┘   └─────────────────┘   └─────────────────┘
src              └──┘         └──────────┘   └─────────────────┘   └─────────────────┘
typ              └──┘        └──────────┘   └─────────────────┘   └─────────────────┘
362  
363  @[simp] theorem factors_mul (a b : associates α) : (a * b).factors = a.factors + b.factors :=
id                                      └────────┘         └─────┘   └──────┘  └──────┘
src                                     └────────┘            └─────┘    └──────┘   └──────┘
typ                                     └────────┘         └─────┘   └──────┘  └──────┘
doc    └──┘
364  eq_of_prod_eq_prod $ eq_of_factors_eq_factors $
id   └────────────────┘   └──────────────────────┘
src  └────────────────┘   └──────────────────────┘
typ  └────────────────┘   └──────────────────────┘
365    by rw [prod_add, factors_prod, factors_prod, factors_prod]
id            └──────┘  └──────────┘  └──────────┘  └──────────┘
src       └──┘└──────┘└┘└──────────┘└┘└──────────┘└┘└──────────┘└─
typ       └──┘└──────┘└┘└──────────┘└┘└──────────┘└┘└──────────┘└─
doc       └──┘        └┘            └┘            └┘            └─
txt       └──┘        └┘            └┘            └┘            └─
par       └──┘        └┘            └┘            └┘            └─
pid         └┘        └┘            └┘            └┘            
st       └───────────┘└────────────┘└────────────┘└────────────┘
366  
src  
typ  
doc  
txt  
par  
pid  
st   
367  theorem factors_mono : ∀{a b : associates α}, a ≤ b → a.factors ≤ b.factors
id                                 └────────┘         └──────┘  └──────┘
src                                 └────────┘             └──────┘   └──────┘
typ                                └────────┘         └──────┘  └──────┘
368  | s t ⟨d, rfl⟩ := by rw [factors_mul] ; exact le_add_of_nonneg_right' bot_le
id             └─┘            └─────────┘          └─────────────────────┘ └────┘
src            └─┘        └──┘└─────────┘└┘  └────┘└─────────────────────┘└────┘
typ            └─┘        └──┘└─────────┘└┘  └────┘└─────────────────────┘└────┘
doc                       └──┘           └┘  └────┘                             
txt                       └──┘           └┘  └────┘                             
par                       └──┘           └┘  └────┘                             
pid                         └┘                                               
st                       └──────────────┘└───────────────────────────────────────
369  
src  
typ  
doc  
txt  
par  
pid  
st   
370  theorem factors_le {a b : associates α} : a.factors ≤ b.factors ↔ a ≤ b :=
id                             └────────┘     └──────┘  └──────┘    
src                            └────────┘       └──────┘   └──────┘    
typ                            └────────┘     └──────┘  └──────┘    
371  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
372    (assume h, have a.factors.prod ≤ b.factors.prod, from prod_mono h,
id                    └──────┘└───┘  └──────┘└───┘       └───────┘ 
src                     └──────┘└───┘   └──────┘└───┘       └───────┘
typ                   └──────┘└───┘  └──────┘└───┘       └───────┘ 
373      by rwa [factors_prod, factors_prod] at this)
id               └──────────┘  └──────────┘
src         └───┘└──────────┘└┘└──────────┘└───────┘
typ         └───┘└──────────┘└┘└──────────┘└───────┘
doc         └───┘            └┘            └───────┘
txt         └───┘            └┘            └───────┘
par         └───┘            └┘            └───────┘
pid            └┘            └┘            └──────┘
st         └────────────────┘└────────────┘└──────┘
374    factors_mono
id     └──────────┘
src    └──────────┘
typ    └──────────┘
375  
376  theorem prod_le {a b : factor_set α} : a.prod ≤ b.prod ↔ a ≤ b :=
id                          └────────┘     └───┘  └───┘    
src                         └────────┘       └───┘   └───┘    
typ                         └────────┘     └───┘  └───┘    
doc                         └────────┘
377  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
378    (assume h, have a.prod.factors ≤ b.prod.factors, from factors_mono h,
id                    └───┘└──────┘  └───┘└──────┘       └──────────┘ 
src                     └───┘└──────┘   └───┘└──────┘       └──────────┘
typ                   └───┘└──────┘  └───┘└──────┘       └──────────┘ 
379      by rwa [prod_factors, prod_factors] at this)
id               └──────────┘  └──────────┘
src         └───┘└──────────┘└┘└──────────┘└───────┘
typ         └───┘└──────────┘└┘└──────────┘└───────┘
doc         └───┘            └┘            └───────┘
txt         └───┘            └┘            └───────┘
par         └───┘            └┘            └───────┘
pid            └┘            └┘            └──────┘
st         └────────────────┘└────────────┘└──────┘
380    prod_mono
id     └───────┘
src    └───────┘
typ    └───────┘
381  
382  instance : has_sup (associates α) := ⟨λa b, (a.factors ⊔ b.factors).prod⟩
id              └─────┘  └────────┘            └──────┘  └──────┘ └──┘
src             └─────┘  └────────┘                └──────┘   └──────┘ └──┘
typ             └─────┘  └────────┘            └──────┘  └──────┘ └──┘
doc             └─────┘
383  instance : has_inf (associates α) := ⟨λa b, (a.factors ⊓ b.factors).prod⟩
id              └─────┘  └────────┘            └──────┘  └──────┘ └──┘
src             └─────┘  └────────┘                └──────┘   └──────┘ └──┘
typ             └─────┘  └────────┘            └──────┘  └──────┘ └──┘
doc             └─────┘
384  
385  instance : bounded_lattice (associates α) :=
id              └─────────────┘  └────────┘ 
src             └─────────────┘  └────────┘
typ             └─────────────┘  └────────┘ 
doc             └─────────────┘
386  { sup          := (⊔),
id                     
src                    
typ                    
387    inf          := (⊓),
id                     
src                    
typ                    
388    sup_le       :=
389      assume a b c hac hbc, factors_prod c ▸ prod_mono (sup_le (factors_mono hac) (factors_mono hbc)),
id                 └─┘ └─┘  └──────────┘   └───────┘  └────┘  └──────────┘ └─┘   └──────────┘ └─┘
src                            └──────────┘    └───────┘  └────┘  └──────────┘       └──────────┘
typ                └─┘ └─┘  └──────────┘   └───────┘  └────┘  └──────────┘ └─┘   └──────────┘ └─┘
390    le_sup_left  := assume a b,
id                             
typ                            
391      le_trans (le_of_eq (factors_prod a).symm) $ prod_mono $ le_sup_left,
id       └──────┘  └──────┘  └──────────┘  └──┘     └───────┘   └─────────┘
src      └──────┘  └──────┘  └──────────┘   └──┘     └───────┘   └─────────┘
typ      └──────┘  └──────┘  └──────────┘  └──┘     └───────┘   └─────────┘
392    le_sup_right := assume a b,
id                             
typ                            
393      le_trans (le_of_eq (factors_prod b).symm) $ prod_mono $ le_sup_right,
id       └──────┘  └──────┘  └──────────┘  └──┘     └───────┘   └──────────┘
src      └──────┘  └──────┘  └──────────┘   └──┘     └───────┘   └──────────┘
typ      └──────┘  └──────┘  └──────────┘  └──┘     └───────┘   └──────────┘
394    le_inf :=
395      assume a b c hac hbc, factors_prod a ▸ prod_mono (le_inf (factors_mono hac) (factors_mono hbc)),
id                 └─┘ └─┘  └──────────┘   └───────┘  └────┘  └──────────┘ └─┘   └──────────┘ └─┘
src                            └──────────┘    └───────┘  └────┘  └──────────┘       └──────────┘
typ                └─┘ └─┘  └──────────┘   └───────┘  └────┘  └──────────┘ └─┘   └──────────┘ └─┘
396    inf_le_left  := assume a b,
id                             
typ                            
397      le_trans (prod_mono inf_le_left) (le_of_eq (factors_prod a)),
id       └──────┘  └───────┘ └─────────┘   └──────┘  └──────────┘ 
src      └──────┘  └───────┘ └─────────┘   └──────┘  └──────────┘
typ      └──────┘  └───────┘ └─────────┘   └──────┘  └──────────┘ 
398    inf_le_right := assume a b,
id                             
typ                            
399      le_trans (prod_mono inf_le_right) (le_of_eq (factors_prod b)),
id       └──────┘  └───────┘ └──────────┘   └──────┘  └──────────┘ 
src      └──────┘  └───────┘ └──────────┘   └──────┘  └──────────┘
typ      └──────┘  └───────┘ └──────────┘   └──────┘  └──────────┘ 
400    .. associates.partial_order,
id        └──────────────────────┘
src       └──────────────────────┘
typ       └──────────────────────┘
401    .. associates.lattice.order_top,
id        └──────────────────────────┘
src       └──────────────────────────┘
typ       └──────────────────────────┘
402    .. associates.lattice.order_bot }
id        └──────────────────────────┘
src       └──────────────────────────┘
typ       └──────────────────────────┘
403  
404  lemma sup_mul_inf (a b : associates α) : (a ⊔ b) * (a ⊓ b) = a * b :=
id                            └────────┘                   
src                           └────────┘                        
typ                           └────────┘                   
405  show (a.factors ⊔ b.factors).prod * (a.factors ⊓ b.factors).prod = a * b,
id         └──────┘  └──────┘ └──┘    └──────┘  └──────┘ └──┘     
src         └──────┘   └──────┘ └──┘     └──────┘   └──────┘ └──┘     
typ        └──────┘  └──────┘ └──┘    └──────┘  └──────┘ └──┘     
406  begin
st   └─────
407    refine eq_of_factors_eq_factors _,
id            └──────────────────────┘
src    └─────┘└──────────────────────┘└┘
typ    └─────┘└──────────────────────┘└┘
doc    └─────┘                        └┘
txt    └─────┘                        └┘
par    └─────┘                        └┘
pid                                  └┘
st   ──────────────────────────────────┘└─
408    rw [← prod_add, prod_factors, factors_mul, factor_set.sup_add_inf_eq_add]
id           └──────┘  └──────────┘  └─────────┘  └───────────────────────────┘
src    └────┘└──────┘└┘└──────────┘└┘└─────────┘└┘└───────────────────────────┘└┘
typ    └────┘└──────┘└┘└──────────┘└┘└─────────┘└┘└───────────────────────────┘└┘
doc    └────┘        └┘            └┘           └┘                             └┘
txt    └────┘        └┘            └┘           └┘                             └┘
par    └────┘        └┘            └┘           └┘                             └┘
pid      └──┘        └┘            └┘           └┘                             
st   ───────────────┘└────────────┘└───────────┘└─────────────────────────────┘
409  end
st   └─┘
410  
411  end associates
412  
413  section
414  open associates unique_factorization_domain lattice
415  
416  /-- `to_gcd_domain` constructs a GCD domain out of a unique factorization domain over a normalization
417  domain. -/
418  def unique_factorization_domain.to_gcd_domain
419    (α : Type*) [normalization_domain α] [unique_factorization_domain α] [decidable_eq (associates α)] :
id                  └──────────────────┘    └─────────────────────────┘    └──────────┘  └────────┘ 
src                 └──────────────────┘     └─────────────────────────┘     └──────────┘  └────────┘
typ                 └──────────────────┘    └─────────────────────────┘    └──────────┘  └────────┘ 
doc                 └──────────────────┘     └─────────────────────────┘
420    gcd_domain α :=
id     └────────┘ 
src    └────────┘
typ    └────────┘ 
doc    └────────┘
421  { gcd := λa b, (associates.mk a ⊓ associates.mk b).out,
id                 └───────────┘   └───────────┘  └─┘
src                  └───────────┘    └───────────┘   └─┘
typ                └───────────┘   └───────────┘  └─┘
422    lcm := λa b, (associates.mk a ⊔ associates.mk b).out,
id                 └───────────┘   └───────────┘  └─┘
src                  └───────────┘    └───────────┘   └─┘
typ                └───────────┘   └───────────┘  └─┘
423    gcd_dvd_left := assume a b, (out_dvd_iff a (associates.mk a ⊓ associates.mk b)).2 $ inf_le_left,
id                                └─────────┘   └───────────┘   └───────────┘       └─────────┘
src                                 └─────────┘    └───────────┘    └───────────┘        └─────────┘
typ                               └─────────┘   └───────────┘   └───────────┘       └─────────┘
424    gcd_dvd_right := assume a b, (out_dvd_iff b (associates.mk a ⊓ associates.mk b)).2 $ inf_le_right,
id                                 └─────────┘   └───────────┘   └───────────┘       └──────────┘
src                                  └─────────┘    └───────────┘    └───────────┘        └──────────┘
typ                                └─────────┘   └───────────┘   └───────────┘       └──────────┘
425    dvd_gcd := assume a b c hac hab, show a ∣ (associates.mk c ⊓ associates.mk b).out,
id                          └─┘ └─┘          └───────────┘   └───────────┘  └─┘
src                                              └───────────┘    └───────────┘   └─┘
typ                         └─┘ └─┘          └───────────┘   └───────────┘  └─┘
426      by rw [dvd_out_iff, le_inf_iff, mk_le_mk_iff_dvd_iff, mk_le_mk_iff_dvd_iff]; exact ⟨hac, hab⟩,
id              └─────────┘  └────────┘  └──────────────────┘  └──────────────────┘          └─┘  └─┘
src         └──┘└─────────┘└┘└────────┘└┘└──────────────────┘└┘└──────────────────┘  └────┘    └┘   
typ         └──┘└─────────┘└┘└────────┘└┘└──────────────────┘└┘└──────────────────┘  └────┘ └─┘└┘└─┘
doc         └──┘           └┘          └┘                    └┘                      └────┘    └┘   
txt         └──┘           └┘          └┘                    └┘                      └────┘    └┘   
par         └──┘           └┘          └┘                    └┘                      └────┘    └┘   
pid           └┘           └┘          └┘                    └┘                               └┘   
st         └──────────────┘└──────────┘└────────────────────┘└────────────────────┘└────────────────┘
427    lcm_zero_left := assume a, show (⊤ ⊔ associates.mk a).out = 0, by simp,
id                                       └───────────┘  └─┘  
src                                       └───────────┘   └─┘         └──┘
typ                                      └───────────┘  └─┘         └──┘
doc                                                                      └──┘
txt                                                                      └──┘
par                                                                      └──┘
st                                                                      └───┘
428    lcm_zero_right := assume a, show (associates.mk a ⊔ ⊤).out = 0, by simp,
id                                      └───────────┘    └─┘  
src                                      └───────────┘     └─┘         └──┘
typ                                     └───────────┘    └─┘         └──┘
doc                                                                       └──┘
txt                                                                       └──┘
par                                                                       └──┘
st                                                                       └───┘
429    gcd_mul_lcm := assume a b,
id                            
typ                           
430      show (associates.mk a ⊓ associates.mk b).out * (associates.mk a ⊔ associates.mk b).out =
id             └───────────┘   └───────────┘  └─┘    └───────────┘   └───────────┘  └─┘  
src            └───────────┘    └───────────┘   └─┘    └───────────┘    └───────────┘   └─┘  
typ            └───────────┘   └───────────┘  └─┘    └───────────┘   └───────────┘  └─┘  
431        normalize (a * b),
id         └───────┘    
src        └───────┘    
typ        └───────┘    
432      by rw [← out_mk, ← out_mul, mul_comm, sup_mul_inf]; refl,
id                └────┘    └─────┘  └──────┘  └─────────┘
src         └────┘└────┘└──┘└─────┘└┘└──────┘└┘└─────────┘  └──┘
typ         └────┘└────┘└──┘└─────┘└┘└──────┘└┘└─────────┘  └──┘
doc         └────┘      └──┘       └┘        └┘             └──┘
txt         └────┘      └──┘       └┘        └┘             └──┘
par         └────┘      └──┘       └┘        └┘             └──┘
pid           └──┘      └──┘       └┘        └┘           
st         └───────────┘└─────────┘└────────┘└───────────┘└────┘
433    normalize_gcd := assume a b, by convert normalize_out _,
id                                           └───────────┘
src                                    └──────┘└───────────┘└┘
typ                                  └──────┘└───────────┘└┘
doc                                    └──────┘             └┘
txt                                    └──────┘             └┘
par                                    └──────┘             └┘
pid                                                        └┘
st                                    └──────────────────────┘
434    .. ‹normalization_domain α› }
id        └──────────────────┘ 
src       └──────────────────┘  
typ       └──────────────────┘ 
doc       └──────────────────┘  
435  
436  end